• 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 completeness proof. 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).
Région Lorraine Grand Nancy