The following tutorials are announced for CAV'01 :
- Pascal
Van Hentenryck "An Overview of Constraint Solving Techniques"
Abstract There is a growing interest in the use of constraint
solving techniques for formal verification of software properties. The goal
of this tutorial is to present an overview of a variety of approaches to
constraint solving. Since most of these techniques approach NP-complete
problems, it is important to understand their strengths and weaknesses to
apply them appropriately on practical problems. As a consequence, the
tutorial will devote time in building intuition on how these techniques prune
the search space to obtain reasonable performance on many problems.
Outline:
- Introduction
- Constraint Solving
- Constraint Techniques in Formal Verification
- Linear Programming
- Integer Programming
- Constraint Programming
- Local Search
- Other Approaches
- Hybrid Constraint Solving Techniques
- Conclusion
- David Basin "Monadic Logics on Strings and Trees"
Abstract: Monadic second-order logics on strings and trees
constitute natural, decidable, yet substantially more expressive,
extensions of Boolean logic. Over the past 8 years, a number of groups
have implemented decision procedures and other tools for these logics
and successfully applied them to a wide variety of problems including
modeling and verifying protocols, parameterized circuits, properties
of programs operating on strings and trees, and even enforcing design
constraints in object-oriented programming. In this tutorial we
motivate, describe, and explore applications for these logics as well
as survey tool support and recently developed procedures for model
generation.
Topics covered: (Chapter Headers)
- Syntax/semantics/decidability.
- Applications: hardware, protocols, constraint checking.
- Connections to regular model checking.
- Tool support: decision procedures, high-level languages,
HOL-embeddings, model generation.
Last modified on 4th May 2001 - cav01@lsv.ens-cachan.fr