---
abstract: "This paper summarises roughly ten years of experience using declarative programming for\r\n developing tools to validate formal specifications.\r\nMore precisely, we present  insights gained and lessons learned while implementing animators and model checkers in Prolog for various specification languages,\r\n  ranging from process algebras such as CSP to model-based specifications such as Z and B."
accompaniment: []
book_title: Proceedings of PPDP'2008
commentary: ~
completion_time: ~
composition_type: ~
conductors_id: []
conductors_name: []
contact_email: ~
copyright_holders: []
corp_creators: []
creators_id:
  - leuschel@cs.uni-duesseldorf.de
creators_name:
  - family: Leuschel
    given: Michael
    honourific: ''
    lineage: ''
data_type: ~
date: 2008
date_type: published
datestamp: 2008-11-04 08:50:29
department: ~
dir: disk0/00/00/00/42
divisions: []
edit_lock_since: ~
edit_lock_until: ~
edit_lock_user: ~
editors_id: []
editors_name: []
eprint_status: archive
eprintid: 42
event_dates: ~
event_location: ~
event_title: ~
event_type: ~
exhibitors_id: []
exhibitors_name: []
fileinfo: /style/images/fileicons/application_pdf.png;/42/1/ppdp8k%2Dleuschel.pdf
full_text_status: public
funders: []
id_number: ~
importid: ~
institution: ~
isbn: ~
ispublished: pub
issn: ~
item_issues_comment: []
item_issues_count: 0
item_issues_description: []
item_issues_id: []
item_issues_reported_by: []
item_issues_resolved_by: []
item_issues_status: []
item_issues_timestamp: []
item_issues_type: []
keywords: ~
lastmod: 2010-04-19 15:05:50
latitude: ~
learning_level: ~
longitude: ~
lyricists_id: []
lyricists_name: []
metadata_visibility: show
monograph_type: ~
note: ~
num_pieces: ~
number: ~
official_url: ~
output_media: ~
pagerange: ~
pages: ~
patent_applicant: ~
pedagogic_type: ~
place_of_pub: ~
pres_type: ~
producers_id: []
producers_name: []
projects:
  - Deploy
publication: ~
publisher: ACM Press
refereed: FALSE
referencetext: ~
related_url_type: []
related_url_url: []
relation_type: []
relation_uri: []
rev_number: 21
series: ~
skill_areas: []
source: ~
status_changed: 2008-11-04 09:43:08
subjects:
  - deploy_tooldev
succeeds: ~
suggestions: ~
sword_depositor: ~
sword_slug: ~
task_purpose: ~
thesis_type: ~
title: 'Declarative Programming for Verification: Lessons and Outlook'
type: book_section
userid: 12
volume: ~
<script src='//archive-bar.soton.ac.uk/archive-bar.js'></script>
