08:45-10:30
IWIL papers
|
- Interactive Verification of Concurrent Systems using Symbolic Execution
Michael Balser, Simon Bäumler, Gerhard Schellhorn and Wolfgang Reif
- Learning Techniques for Pseudo-Boolean Solving
Jose Santos and Vasco Manquinho
- Complete Pruning Methods and a Practical Search Strategy for SOL
Hidetomo Nabeshima, Koji Iwanuma and Katsumi Inoue
|
| 10:30-11:00
| Break
|
11:00-11:35
IWIL paper
|
- Proofs and Refutations, and Z3
Leonardo de Moura and Nikolaj Bjørner
|
| 11:35-11:45
| Get more coffee
|
11:45-12:45
Invited talk
|
- Automated Reasoning for Mizar: Artificial Intelligence through Knowledge Exchange
Josef Urban
|
| 12:45-14:15
| Lunch
|
14:15-16:00
KEAPPA papers
|
- A TLA+ Proof System
Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport and Stephan Merz
- The SZS Ontologies for Automated Reasoning Software
Geoff Sutcliffe
- An Exchange Format for Modular Knowledge
Florian Rabe and Michael Kohlhase
|
| 16:00-16:30
| Break
|
16:30-17:40
KEAPPA papers
|
- Connecting Gröbner Bases Programs with Coq to do Proofs in Algebra, Geometry and Arithmetics
Loïc Pottier
- Transforming and Analyzing Proofs in the CERES-system
Stefan Hetzl, Alexander Leitsch, Daniel Weller and Bruno Woltzenlogel Paleo
|