• Erika Ábrahám, John Abbott, Bernd Becker, Anna M. Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, and Thomas Sturm, "Satisfiability Checking and Symbolic Computation", (2016), pp. 3 p.  
    Citation
    Erika Ábrahám, John Abbott, Bernd Becker, Anna M. Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, and Thomas Sturm, "Satisfiability Checking and Symbolic Computation", (2016), pp. 3 p.
    Abstract
    Symbolic Computation and Satisfiability Checking are viewed as individual research areas, but they share common interests in the development, implementation and application of decision procedures for arithmetic theories. Despite these commonalities, the two communities are currently only weakly connected. We introduce a new project SC-square to build a joint community in this area, supported by a newly accepted EU (H2020-FETOPEN-CSA) project of the same name. We aim to strengthen the connection between these communities by creating common platforms, initiating interaction and exchange, identifying common challenges, and developing a common roadmap. This abstract and accompanying poster describes the motivation and aims for the project, and reports on the first activities.
    Export
  • Erika Ábrahám, John Abbott, Bernd Becker, Anna M. Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, and Thomas Sturm, "SC2: Satisfiability Checking meets Symbolic Computation (Project Paper)", (2016), pp. 15 p.  
    Citation
    Erika Ábrahám, John Abbott, Bernd Becker, Anna M. Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, and Thomas Sturm, "SC2: Satisfiability Checking meets Symbolic Computation (Project Paper)", (2016), pp. 15 p.
    Abstract
    Symbolic Computation and Satisfiability Checking are two research areas, both having their individual scientific focus but sharing also common interests in the development, implementation and application of decision procedures for arithmetic theories. Despite their commonalities, the two communities are rather weakly connected. The aim of our newly accepted SC-square project (H2020-FETOPEN-CSA) is to strengthen the connection between these communities by creating common platforms, initiating interaction and exchange, identifying common challenges, and developing a common roadmap from theory along the way to tools and (industrial) applications. In this paper we report on the aims and on the first activities of this project, and formalise some relevant challenges for the unified SC-square community.
    Export
  • Erika Ábrahám, John Abbott, Bernd Becker, Anna M. Bigatti, Martin Brain, Bruno Buchberger, Allesandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, and Thomas Sturm, "SC2: Satisfiability Checking Meets Symbolic Computation", in Intelligent Computer Mathematics, edited by Michael Kohlhase, Moa Johansson, Bruce Miller, Leonardo de Moura, and Frank Tompa (Springer, Berlin, 2016), pp. 28-43.  
    Citation
    Erika Ábrahám, John Abbott, Bernd Becker, Anna M. Bigatti, Martin Brain, Bruno Buchberger, Allesandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, and Thomas Sturm, "SC2: Satisfiability Checking Meets Symbolic Computation", in Intelligent Computer Mathematics, edited by Michael Kohlhase, Moa Johansson, Bruce Miller, Leonardo de Moura, and Frank Tompa (Springer, Berlin, 2016), pp. 28-43.
    Export
  • Erika Ábrahám, John Abbott, Bernd Becker, Anna M. Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, and Thomas Sturm, "Satisfiability Checking and Symbolic Computation," ACM Communications in Computer Algebra 50 (4), 145-147 (2016).  
    Citation
    Erika Ábrahám, John Abbott, Bernd Becker, Anna M. Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, and Thomas Sturm, "Satisfiability Checking and Symbolic Computation," ACM Communications in Computer Algebra 50 (4), 145-147 (2016).
    Export
  • Ernst Althaus, Björn Beber, Werner Damm, Stefan Disch, Willem Hagemann, Astrid Rakow, Christoph Scholl, Uwe Waldmann, and Boris Wirtz, "Verification of Linear Hybrid Systems with Large Discrete State Spaces: Exploring the Design Space for Optimization", in AVACS Technical Report, (2016), Vol. 103, pp. 93 p.  
    Citation
    Ernst Althaus, Björn Beber, Werner Damm, Stefan Disch, Willem Hagemann, Astrid Rakow, Christoph Scholl, Uwe Waldmann, and Boris Wirtz, "Verification of Linear Hybrid Systems with Large Discrete State Spaces: Exploring the Design Space for Optimization", in AVACS Technical Report, (2016), Vol. 103, pp. 93 p.
    Abstract
    This paper provides a suite of optimization techniques for the verification of safety properties of linear hybrid automata with large discrete state spaces, such as naturally arising when incorporating health state monitoring and degradation levels into the controller design. Such models can -- in contrast to purely functional controller models -- not analyzed with hybrid verification engines relying on explicit representations of modes, but require fully symbolic representations for both the continuous and discrete part of the state space. The optimization techniques shown yield consistently a speedup of about 20 against previously published results for a similar benchmark suite, and complement these with new results on counterexample guided abstraction refinement. In combination with the methods guaranteeing preciseness of abstractions, this allows to significantly extend the class of models for which safety can be established, covering in particular models with 23 continuous variables and 2 to the 71 discrete states, 20 continuous variables and 2 to the 199 discrete states, and 9 continuous variables and 2 to the 271 discrete states.
    Export
  • Noran Azmy, A Machine-checked Proof of Correctness of Pastry, PhD Thesis, Universität des Saarlandes, 2016.  
    Citation
    Noran Azmy, A Machine-checked Proof of Correctness of Pastry, PhD Thesis, Universität des Saarlandes, 2016.
    Abstract
    A distributed hash table (DHT) is a peer-to-peer network that offers the function of a classic hash table, but where different key-value pairs are stored at different nodes on the network. Like a classic hash table, the main function provided by a DHT is key lookup, which retrieves the value stored at a given key. Examples of DHT protocols include Chord, Pastry, Kademlia and Tapestry. Such DHT protocols certain correctness and performance guarantees, but formal verification typically discovers border cases that violate those guarantees. In his PhD thesis, Tianxiang Lu reported correctness problems in published versions of Pastry and developed a model called LuPastry, for which he provided a partial proof of correct delivery of lookup messages assuming no node failure, mechanized in the TLA+ Proof System. In analyzing Lu's proof, I discovered that it contained unproven assumptions, and found counterexamples to several of these assumptions. The contribution of this thesis is threefold. First, I present LuPastry+, a revised TLA+ specification of LuPastry. Aside from needed bug fixes, LuPastry+ contains new definitions that make the specification more modular and significantly improve proof automation. Second, I present a complete TLA+ proof of correct delivery for LuPastry+. Third, I prove that the final step of the node join process of LuPastry/LuPastry+ is not necessary to achieve consistency. In particular, I develop a new specification with a simpler node join process, which I denote by Simplified LuPastry+, and prove correct delivery of lookup messages for this new specification. The proof of correctness of Simplified LuPastry+ is written by reusing the proof for LuPastry+, which represents a success story in proof reuse, especially for proofs of this size. Each of the two proofs amounts to over 32,000 proof steps; to my knowledge, they are currently the largest proofs written in the TLA+ language, and---together with Lu's proof---the only examples of applying full theorem proving for the verification of DHT protocols
    Export
  • Noran Azmy, Stephan Merz, and Christoph Weidenbach, "A Rigorous Correctness Proof for Pastry", in Abstract State Machines, Alloy, B, TLA, VDM, and Z, edited by Michael Butler, Klaus-Dieter Schewe, Atif Mashkoor, and Miklos Biro (Springer, Berlin, 2016), pp. 86-101.  
    Citation
    Noran Azmy, Stephan Merz, and Christoph Weidenbach, "A Rigorous Correctness Proof for Pastry", in Abstract State Machines, Alloy, B, TLA, VDM, and Z, edited by Michael Butler, Klaus-Dieter Schewe, Atif Mashkoor, and Miklos Biro (Springer, Berlin, 2016), pp. 86-101.
    Export
  • Moulay A. Barkatou, Maximilian Jaroschek, and Suzy S. Maddah, "Formal Solutions of Completely Integrable Pfaffian Systems With Normal Crossings," Journal of Symbolic Computation 81, 41-68 (2017).  
    Citation
    Moulay A. Barkatou, Maximilian Jaroschek, and Suzy S. Maddah, "Formal Solutions of Completely Integrable Pfaffian Systems With Normal Crossings," Journal of Symbolic Computation 81, 41-68 (2017).
    Export
  • Jasmin Christian Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, and Albert Steckermeier, "Semi-intelligible Isar Proofs from Machine-Generated Proofs," Journal of Automated Reasoning 56 (2), 155-200 (2016).  
    Citation
    Jasmin Christian Blanchette, Sascha Böhme, Mathias Fleury, Steffen Juilf Smolka, and Albert Steckermeier, "Semi-intelligible Isar Proofs from Machine-Generated Proofs," Journal of Automated Reasoning 56 (2), 155-200 (2016).
    Export
  • Jasmin Christian Blanchette, Mathias Fleury, and Christoph Weidenbach, "A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality", in Automated Reasoning, edited by Nicola Olivetti and Ashish Tiwari (Springer, Berlin, 2016), pp. 25-44.  
    Citation
    Jasmin Christian Blanchette, Mathias Fleury, and Christoph Weidenbach, "A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality", in Automated Reasoning, edited by Nicola Olivetti and Ashish Tiwari (Springer, Berlin, 2016), pp. 25-44.
    Export
  • Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef Urban, "A Learning-Based Fact Selector for Isabelle/HOL," Journal of Automated Reasoning 57 (3), 219-244 (2016).  
    Citation
    Jasmin Christian Blanchette, David Greenaway, Cezary Kaliszyk, Daniel Kühlwein, and Josef Urban, "A Learning-Based Fact Selector for Isabelle/HOL," Journal of Automated Reasoning 57 (3), 219-244 (2016).
    Export
  • Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban, "Hammering towards QED," Journal of Formalized Reasoning 9 (1), 101-148 (2016).  
    Citation
    Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban, "Hammering towards QED," Journal of Formalized Reasoning 9 (1), 101-148 (2016).
    Export
  • Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel, "Soundness and Completeness Proofs by Coinductive Methods," Journal of Automated Reasoning 58 (1), 149-179 (2017).  
    Citation
    Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel, "Soundness and Completeness Proofs by Coinductive Methods," Journal of Automated Reasoning 58 (1), 149-179 (2017).
    Export
  • Jasmin Christian Blanchette and Stephan Merz (eds), Interactive Theorem Proving. (Springer, Berlin, 2016).  
    Citation
    Jasmin Christian Blanchette and Stephan Merz (eds), Interactive Theorem Proving. (Springer, Berlin, 2016).
    Export
  • Jasmin Christian Blanchette and Cezary Kaliszyk (eds), Proceedings First International Workshop on Hammers for Type Theories. (2016).  
    Citation
    Jasmin Christian Blanchette and Cezary Kaliszyk (eds), Proceedings First International Workshop on Hammers for Type Theories. (2016).
    Export
  • Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, and Nicholas Smallbone, "Encoding Monomorphic and Polymorphic Types", (2016), pp. LMCS-2014-1018.  
    Citation
    Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, and Nicholas Smallbone, "Encoding Monomorphic and Polymorphic Types", (2016), pp. LMCS-2014-1018.
    Abstract
    Many automatic theorem provers are restricted to untyped logics, and existing translations from typed logics are bulky or unsound. Recent research proposes monotonicity as a means to remove some clutter when translating monomorphic to untyped first-order logic. Here we pursue this approach systematically, analysing formally a variety of encodings that further improve on efficiency while retaining soundness and completeness. We extend the approach to rank-1 polymorphism and present alternative schemes that lighten the translation of polymorphic symbols based on the novel notion of "cover". The new encodings are implemented in Isabelle/HOL as part of the Sledgehammer tool. We include informal proofs of soundness and correctness, and have formalised the monomorphic part of this work in Isabelle/HOL. Our evaluation finds the new encodings vastly superior to previous schemes.
    Export
  • Martin Bromberger and Christoph Weidenbach, "Fast Cube Tests for LIA Constraint Solving", in Automated Reasoning, edited by Nicola Olivetti and Ashish Tiwari (Springer, Berlin, 2016), pp. 116-132.  
    Citation
    Martin Bromberger and Christoph Weidenbach, "Fast Cube Tests for LIA Constraint Solving", in Automated Reasoning, edited by Nicola Olivetti and Ashish Tiwari (Springer, Berlin, 2016), pp. 116-132.
    Export
  • Martin Bromberger and Christoph Weidenbach, "Computing a Complete Basis for Equalities Implied by a System of LRA Constraints", in Satisfiability Modulo Theories, edited by Tim King and Ruzica Piskac (CEUR-WS.org, Aachen, 2016), pp. 15-30.  
    Citation
    Martin Bromberger and Christoph Weidenbach, "Computing a Complete Basis for Equalities Implied by a System of LRA Constraints", in Satisfiability Modulo Theories, edited by Tim King and Ruzica Piskac (CEUR-WS.org, Aachen, 2016), pp. 15-30.
    Export
  • Martin Bromberger, Analysis and Implementation of LIA solvers: CutSAT and BBSAT, Master Thesis, Universität des Saarlandes, 2016.  
    Citation
    Martin Bromberger, Analysis and Implementation of LIA solvers: CutSAT and BBSAT, Master Thesis, Universität des Saarlandes, 2016.
    Export
  • Simon Cruanes and Jasmin Christian Blanchette, "Extending Nunchaku to Dependent Type Theory", in Proceedings First International Workshop on Hammers for Type Theories, edited by Jasmin Christian Blanchette and Cezary Kaliszyk (2016), pp. 10 p.  
    Citation
    Simon Cruanes and Jasmin Christian Blanchette, "Extending Nunchaku to Dependent Type Theory", in Proceedings First International Workshop on Hammers for Type Theories, edited by Jasmin Christian Blanchette and Cezary Kaliszyk (2016), pp. 10 p.
    Abstract
    Nunchaku is a new higher-order counterexample generator based on a sequence of transformations from polymorphic higher-order logic to first-order logic. Unlike its predecessor Nitpick for Isabelle, it is designed as a stand-alone tool, with frontends for various proof assistants. In this short paper, we present some ideas to extend Nunchaku with partial support for dependent types and type classes, to make frontends for Coq and other systems based on dependent type theory more useful.
    Export
  • Stéphane Demri, Deepak Kapur, and Christoph Weidenbach, "Preface -Special Issue of Selected Extended Papers of IJCAR 2014," Journal of Automated Reasoning 58 (1), 1-2 (2017).  
    Citation
    Stéphane Demri, Deepak Kapur, and Christoph Weidenbach, "Preface -Special Issue of Selected Extended Papers of IJCAR 2014," Journal of Automated Reasoning 58 (1), 1-2 (2017).
    Export
  • Christof Fetzer, Christoph Weidenbach, and Patrick Wischnewski, "Compliance, Functional Safety and Fault Detection by Formal Methods", in Leveraging Applications of Formal Methods, Verification and Validation, edited by Tiziana Margaria and Bernhard Steffen (Springer, Berlin, 2016), pp. 626-632.  
    Citation
    Christof Fetzer, Christoph Weidenbach, and Patrick Wischnewski, "Compliance, Functional Safety and Fault Detection by Formal Methods", in Leveraging Applications of Formal Methods, Verification and Validation, edited by Tiziana Margaria and Bernhard Steffen (Springer, Berlin, 2016), pp. 626-632.
    Export
  • Marek Košta, Thomas Sturm, and Andreas Dolzmann, "Better Answers to Real Questions," Journal of Symbolic Computation 74, 255-275 (2016).  
    Citation
    Marek Košta, Thomas Sturm, and Andreas Dolzmann, "Better Answers to Real Questions," Journal of Symbolic Computation 74, 255-275 (2016).
    Abstract
    We consider existential problems over the reals. Extended quantifier elimination generalizes the concept of regular quantifier elimination by providing in addition answers, which are descriptions of possible assignments for the quantified variables. Implementations of extended quantifier elimination via virtual substitution have been successfully applied to various problems in science and engineering. So far, the answers produced by these implementations included infinitesimal and infinite numbers, which are hard to interpret in practice. We introduce here a post-processing procedure to convert, for fixed parameters, all answers into standard real numbers. The relevance of our procedure is demonstrated by application of our implementation to various examples from the literature, where it significantly improves the quality of the results.
    Export
  • Marek Košta, New Concepts for Real Quantifier Elimination by Virtual Substitution, PhD Thesis, Universität des Saarlandes, 2016.  
    Citation
    Marek Košta, New Concepts for Real Quantifier Elimination by Virtual Substitution, PhD Thesis, Universität des Saarlandes, 2016.
    Export
  • Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, and Cesare Tinelli, "Model Finding for Recursive Functions in SMT", in Automated Reasoning, edited by Nicola Olivetti and Ashish Tiwari (Springer, Berlin, 2016), pp. 133-151.  
    Citation
    Andrew Reynolds, Jasmin Christian Blanchette, Simon Cruanes, and Cesare Tinelli, "Model Finding for Recursive Functions in SMT", in Automated Reasoning, edited by Nicola Olivetti and Ashish Tiwari (Springer, Berlin, 2016), pp. 133-151.
    Export
  • Andrew Reynolds and Jasmin Christian Blanchette, "A Decision Procedure for (Co)datatypes in SMT Solvers", in Twenty-Fifth International Joint Conference on Artificial Intelligence, edited by Subbarao Kambhampati (AAAI, Palo Alto, CA, 2016), pp. 4205-4209.  
    Citation
    Andrew Reynolds and Jasmin Christian Blanchette, "A Decision Procedure for (Co)datatypes in SMT Solvers", in Twenty-Fifth International Joint Conference on Artificial Intelligence, edited by Subbarao Kambhampati (AAAI, Palo Alto, CA, 2016), pp. 4205-4209.
    Export
  • Thomas Sturm, Marco Voigt, and Christoph Weidenbach, "Deciding First-Order Satisfiability when Universal and Existential Variables are Separated", in Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, (ACM, New York, NY, 2016), pp. 86-95.  
    Citation
    Thomas Sturm, Marco Voigt, and Christoph Weidenbach, "Deciding First-Order Satisfiability when Universal and Existential Variables are Separated", in Proceedings of the 31st Annual ACM-IEEE Symposium on Logic in Computer Science, (ACM, New York, NY, 2016), pp. 86-95.
    Export
  • Thomas Sturm, Marco Voigt, and Christoph Weidenbach, "Deciding First-Order Satisfiability when Universal and Existential Variables are Separated", (2016), pp. 23 p.  
    Citation
    Thomas Sturm, Marco Voigt, and Christoph Weidenbach, "Deciding First-Order Satisfiability when Universal and Existential Variables are Separated", (2016), pp. 23 p.
    Abstract
    We introduce a new decidable fragment of first-order logic with equality, which strictly generalizes two already well-known ones -- the Bernays-Sch\"onfinkel-Ramsey (BSR) Fragment and the Monadic Fragment. The defining principle is the syntactic separation of universally quantified variables from existentially quantified ones at the level of atoms. Thus, our classification neither rests on restrictions on quantifier prefixes (as in the BSR case) nor on restrictions on the arity of predicate symbols (as in the monadic case). We demonstrate that the new fragment exhibits the finite model property and derive a non-elementary upper bound on the computing time required for deciding satisfiability in the new fragment. For the subfragment of prenex sentences with the quantifier prefix $\exists^* \forall^* \exists^*$ the satisfiability problem is shown to be complete for NEXPTIME. Finally, we discuss how automated reasoning procedures can take advantage of our results.
    Export
  • Ching Hoo Tang and Christoph Weidenbach, "A Dynamic Logic for Configuration", in Proceedings of the 2nd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2016) affiliated with the International Joint Conference on Automated Reasoning (IJCAR 2016), edited by Christoph Benzmüller and Jens Otten (CEUR-WS.org, Aachen, 2016), pp. 36-50.  
    Citation
    Ching Hoo Tang and Christoph Weidenbach, "A Dynamic Logic for Configuration", in Proceedings of the 2nd International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2016) affiliated with the International Joint Conference on Automated Reasoning (IJCAR 2016), edited by Christoph Benzmüller and Jens Otten (CEUR-WS.org, Aachen, 2016), pp. 36-50.
    Export
  • Andreas Teucke and Christoph Weidenbach, "Ordered Resolution with Straight Dismatching Constraints", in Practical Aspects of Automated Reasoning, edited by Pascal Fontaine, Stephan Schulz, and Josef Urban (CEUR-WS.org, Aachen, 2016), pp. 95-109.  
    Citation
    Andreas Teucke and Christoph Weidenbach, "Ordered Resolution with Straight Dismatching Constraints", in Practical Aspects of Automated Reasoning, edited by Pascal Fontaine, Stephan Schulz, and Josef Urban (CEUR-WS.org, Aachen, 2016), pp. 95-109.
    Export
  • Marco Voigt, "Beyond Standard Miniscoping", in Deduktionstreffen 2016, (2016).  
    Citation
    Marco Voigt, "Beyond Standard Miniscoping", in Deduktionstreffen 2016, (2016).
    Export
  • Marco Voigt, "The Complexity of Satisfiability in the Separated Fragment - A Journey Through ELEMENTARY and Beyond", in Seventeenth International Workshop on Logic and Computational Complexity, (2016), pp. 43-47.  
    Citation
    Marco Voigt, "The Complexity of Satisfiability in the Separated Fragment - A Journey Through ELEMENTARY and Beyond", in Seventeenth International Workshop on Logic and Computational Complexity, (2016), pp. 43-47.
    Export
  • Daniel Wand, More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification, Master Thesis, Universität des Saarlandes, 2016.  
    Citation
    Daniel Wand, More SPASS with Isabelle - Superposition with Hard Sorts and Configurable Simplification, Master Thesis, Universität des Saarlandes, 2016.
    Export