Programme
The programme of this seminar included:
- A tutorial on the state of the art of CP to the CAV participants.
- A tutorial on the state of the art of CAV to the CP participants.
- Presentations by the participants on current CAV research based on CP, CAV challenges to CP solvers, etc.
- An excursion on Wednesday afternoon: a so-called "Blue Voyage" by boat around the bay, with time for swimming and a BBQ.
The precise programme was available via Google Docs. It remained flexible, in order to account for unforeseen developments during the seminar.
Talks
Monday
- Helmut Simonis
Tutorial - CP by Systematic Search Over Discrete Finite Domains
[pdf] - Pierre Flener
Tutorial - CP by Local Search
[pdf] - Michel Rueher
Tutorial - CP by Systematic Search Over Real-Number and Floating-Point Domains
[pdf] - Ahmed Bouajjani
Tutorial - Model Checking
[pdf]
Tuesday
- Shaz Qadeer
Using SMT Solvers for Program Analysis
[pdf] [ppt] - Eyal Bin
Challenges in Hardware Verification
[abstract] [pdf] [ppt]
- Jean-François Raskin
Classical and Non-Classical Applications of SAT Solvers in CAV
[pdf] - Mike Codish
Programming with Boolean Satisfaction
[abstract] [ppt] [pdf]
- Thomas Wies
Use of SMT-Solvers in Verification
[pdf] [ppt] - Michel Rueher
On Search Strategies for Constraint-Based Bounded Model Checking
[pdf] - Hongseok Yang
Abstractions from Tests
[abstract] [pdf]
Wednesday
- Philipp Rümmer
Reasoning for Verification: Theorem Provers, SMT, and Interpolation
[abstract] [pdf]
- Ruzica Piskac
Current Limitations of SAT/SMT-Techniques in Model Checking
[abstract] [pdf] - Vitaly Lagoon
Constraint-Based Random Test Generation
[pdf] - Arnaud Gotlieb
CP also meets Software Testing
[pdf]
Thursday
- Giorgio Delzanno
Constraints for Parameterized Verification
[pdf] - François Fages
On Solving Temporal Logic Constraints in Constrained Transition Systems
[abstract] [pdf] - Gopal Gupta
Using CLP(R) for Verifying Timing Properties of Complex Systems
[pdf] - Enrico Tronci
Quantized Feedback Control Software Synthesis from System-Level Formal Specifications
[abstract] [pdf] - Sébastien Bardin
A Combined Approach for Solving Constraints over Finite Domains and Arrays
[abstract] [pdf] - Peter Habermehl
Parikh Image of Languages
[pdf] - Andreas Podelski
Constraints in Verification
[pdf] - Harald Søndergaard
Local Bit-Precise Reasoning in Program Analysis
[pdf]
Friday
- Tomás Vojnar
Verification of Low-Level List Manipulation
[pdf] - Constantin Enea
Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data
[abstract] [pdf] - Valerio Senni
Program Transformation and Constraint-Based Verification
[abstract] [pdf] - John Gallagher
Constraints in Abstract Model-Checking
[pdf] - Ruzica Piskac
Software Synthesis using Automated Reasoning
[abstract] [pdf]
Related Events
The content of this seminar overlaps with the following ones:
- CSTVA'11, 3rd workshop on Constraints in Software Testing, Verification, and Analysis
- CSTVA'10, 2nd workshop on Constraints in Software Testing, Verification, and Analysis
- CSTVA'06, 1st workshop on Constraints in Software Testing, Verification, and Analysis
- CSPSAT'12, 2nd int'l workshop on the Cross-Fertilization Between CSP and SAT
- CSPSAT'11, 1st int'l workshop on the Cross-Fertilization Between CSP and SAT
- CP'06 Workshop on the Integration of SAT and CP techniques: see the chapter On the First SAT/CP Integration Workshop in the book Trends in Constraint Programming, and see the Special Issue on SAT/CP Integration of Journal on Satisfiability, Boolean Modeling and Computation (scroll to the bottom)
- Hybrid Methods for Constraint Programming, the ACP Summer School 2011: hybridising CP with SAT, SLS, MIP, and global optimisation