- Stéphane Demri (New York University, USA & LSV, CNRS, France), joint with FroCoS 2013
Witness Runs for Counter Machines
We present recent results about the verification
of counter machines by using decision procedures for Presburger arithmetic.
We recall several known classes of counter machines for which
the reachability sets are Presburger-definable as well as
temporal logics with arithmetical constraints.
We discuss issues related to flat counter machines, path schema enumeration
and the use of SMT solvers.
- Sara Negri (University of Helsinki, Finland)
On the duality of proofs and countermodels in labelled sequent calculi
Proofs and countermodels are the two sides of completeness proofs,
but, in general, failure to find one does not automatically give the
other. The limitation is encountered also for decidable non-classical
logics in traditional completeness proofs based on Henkin's method of
maximal consistent sets of formulas.
A method will be presented for unifying proof search and countermodel
construction that is a synthesis of a generation of calculi with
internalized relational semantics and a Tait-Sch\"utte-Takeuti style
The procedure will be illustrated through a number of examples of
non-classical logics, including intermediate logics and their modal
companions, provability logics, knowability logic, and extensions
beyond geometric theories.
A method of finitization of countermodel construction based on
either a search of a minimal derivation, on a syntactic counterpart
of semantic filtration, or on a suitable embedding into provability
logic will be detailed for the special case of intuitionistic logic,
together with its current scope and open challenges.
- Tobias Nipkow (Institut für Informatik, Technische Universität München, Germany)
A Brief Survey of Verified Decision Procedures for Equivalence of Regular Expressions
We survey a number of decision procedures for the equivalence of
regular expressions that have been formalised with the help of
interactive proof assistant over the past few years
(joint work with Maximilian Haslbeck, Institut für Informatik,
Technische Universität München).