Email Gateway (Aug 18 2022 at 09:26): Email Gateway (Aug 18 2022 at 09:26):From: Serge Autexier <autexier@dfki.de>
[Apologies if your receive multiple copies]
[Early registration deadline: Monday, 10 July 2006]
CALL FOR PARTICIPATION
3rd International Verification Workshop (VERIFY'06)
What are the verification problems? What are the deduction techniques?
in connection with IJCAR'06 at FLoC'06
August 15-16, 2006, Seattle, USA
[http://www.easychair.org/FLoC-06/VERIFY.html]
The formal verification of critical information systems has a long
tradition as one of the main areas of application for automated
theorem proving. Nevertheless, the area is of still growing
importance as the number of computers affecting everyday life and the
complexity of these systems are both increasing. The purpose of the
VERIFY workshop series is to discuss problems arising during the
formal modeling and verification of information systems and to
investigate suitable solutions. Possible perspectives include those
of automated theorem proving, tool support, system engineering, and
applications.
The VERIFY workshops aim at bringing together people who are
interested in the development of safety and security critical systems,
in formal methods, in the development of automated theorem proving
techniques, and in the development of tool support. Practical
experiences gained in realistic verifications are of interest to the
automated theorem proving community and new theorem proving techniques
should be transferred into practice. The overall objective of the
VERIFY workshops is to identify open problems and to discuss possible
solutions under the theme
What are the verification problems? What are the deduction techniques?
In 2006, VERIFY will specifically consider issues regarding the
application of "tool support for formal modeling, verification and
stepwise system development" without excluding submissions regarding
other topics in the focus of the workshop. Therefore, submissions in
this area are especially encouraged.
KEYNOTE SPEAKERS
John Rushby (SRI International)
Threatened by a Great Opportunity: Disruptive Innovation in Formal
Verification
Luca Vigano (ETH Zürich)
Automated Reasoning for Security Protocol Analysis
Christoph Walther (TU Darmstadt)
Verification in the Classroom
ACCEPTED PAPERS
Robert Palmer, Ganesh Gopalakrishnan, and Mike Kirby
Formal Specification and Verification Using +CAL: An Experience
Report
Viorica Sofronie-Stokkermans
Local reasoning in verification
Laura Ildiko Kovacs, Tudor Jebelean
Finding Polynomial Invariants for Imperative Loops in the Theorema
System
Bernhard Beckert, Vladimir Klebanov
Must Program Verification Systems and Calculi be Verified?
Dieter Hutter
Automating Proofs of Unwinding Conditions
Andreas Schlosser, Christoph Walther, and Markus Aderhold
Axiomatic Specifications in VeriFun
Achim D. Brucker, Burkhart Wolff
A Package for Extensible Object-Oriented Data Models with an
Application to IMP++
Sara Van Langenhove, Albert Hoogewijs
Verifying Sliced Hierarchical Statecharts with SVtL
Siraj Shaikh, Vicky Bush, and Steve Schneider
A heuristic for constructing rank functions to verify authentication
protocols
Raghavendra Kagalavadi Ramesh, Deepak D'Souza
Checking Unwinding Conditions for Finite State Systems
Myla Archer, Elizabeth Leonard
Establishing High Confidence in Code Implementations of Algorithms
using Formal Verification of Pseudocode
The registration for the workshop is via the FLOC'06 registration
webpage:
http://www.easychair.org/FLoC-06/floc-registration.html
We are looking forward to see you at the workshop!
Serge Autexier & Heiko Mantel
Last updated: May 03 2024 at 12:27 UTC