# Publications

• 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, 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
• 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
• 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
• 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, 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
• 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
• 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 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
• 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, 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
• 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
• Marco Voigt, "The Complexity of Satisfiability in the Separated Fragment - A Journey Through ELEMENTARY and Beyond slides", 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 slides", in Seventeenth International Workshop on Logic and Computational Complexity, (2016), pp. 43-47.
Export
• Hassan Errami, Markus Eiswirth, Dima Grigoriev, Werner M. Seiler, Thomas Sturm, and Andreas Weber, "Detection of Hopf bifurcations in chemical reaction networks using convex coordinates," Journal of Computational Physics 291, 279-302 (2015).
Citation
Hassan Errami, Markus Eiswirth, Dima Grigoriev, Werner M. Seiler, Thomas Sturm, and Andreas Weber, "Detection of Hopf bifurcations in chemical reaction networks using convex coordinates," Journal of Computational Physics 291, 279-302 (2015).
Abstract
We present ecient algorithmic methods to detect Hopf bifurcation xed points in chemical reaction networks with symbolic rate constants, thereby yielding information about the oscillatory behavior of the networks. Our methods use the representations of the systems on convex coordinates that arise from stoichiometric network analysis. One of our methods then reduces the problem of determining the existence of Hopf bifurcation xed points to a rst-order formula over the ordered eld of the reals that can be solved using computational logic packages. The second method uses ideas from tropical geometry to formulate a more ecient method that is incomplete in theory but worked very well for the examples that we have attempted; we have shown it to be able to handle systems involving more than 20 species.
Export
• Gábor Alagi and Christoph Weidenbach, "NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment", in Frontiers of Combining Systems, edited by Carsten Lutz and Silvio Ranise (Springer, Berlin, 2015), pp. 69-84.
Citation
Gábor Alagi and Christoph Weidenbach, "NRCL - A Model Building Approach to the Bernays-Schönfinkel Fragment", in Frontiers of Combining Systems, edited by Carsten Lutz and Silvio Ranise (Springer, Berlin, 2015), pp. 69-84.
Export
• Peter Baumgartner, Joshua Bax, and Uwe Waldmann, "Beagle -- A Hierarchic Superposition Theorem Prover", in Automated Deduction -- CADE-25, edited by Amy P. Felty and Aart Middeldorp (Springer, Berlin, 2015), pp. 367-377.
Citation
Peter Baumgartner, Joshua Bax, and Uwe Waldmann, "Beagle -- A Hierarchic Superposition Theorem Prover", in Automated Deduction -- CADE-25, edited by Amy P. Felty and Aart Middeldorp (Springer, Berlin, 2015), pp. 367-377.
Export
• Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel, "Witnessing (Co)datatypes", in Programming Languages and Systems, edited by Jan Vitek (Springer, Berlin, 2015), pp. 359-382.
Citation
Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel, "Witnessing (Co)datatypes", in Programming Languages and Systems, edited by Jan Vitek (Springer, Berlin, 2015), pp. 359-382.
Export
• Jasmin Christian Blanchette, Maximilian Haslbeck, Daniel Matichuk, and Tobias Nipkow, "Mining the Archive of Formal Proofs", in Intelligent Computer Mathematics, edited by Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge (Springer, Berlin, 2015), pp. 3-17.
Citation
Jasmin Christian Blanchette, Maximilian Haslbeck, Daniel Matichuk, and Tobias Nipkow, "Mining the Archive of Formal Proofs", in Intelligent Computer Mathematics, edited by Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge (Springer, Berlin, 2015), pp. 3-17.
Export
• Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel, "Foundational Extensible Corecursion: A Proof Assistant Perspective", in Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, (ACM, New York, NY, 2015), pp. 192-204.
Citation
Jasmin Christian Blanchette, Andrei Popescu, and Dmitriy Traytel, "Foundational Extensible Corecursion: A Proof Assistant Perspective", in Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, (ACM, New York, NY, 2015), pp. 192-204.
Export
• Jasmin Christian Blanchette and Nikolai Kosmatov (eds), Tests and Proofs. (Springer, Berlin, 2015).
Citation
Jasmin Christian Blanchette and Nikolai Kosmatov (eds), Tests and Proofs. (Springer, Berlin, 2015).
Export
• Martin Bromberger, Thomas Sturm, and Christoph Weidenbach, "Linear Integer Arithmetic Revisited", in Automated Deduction -- CADE-25, edited by Amy P. Felty and Aart Middeldorp (Springer, Berlin, 2015), pp. 623-637.
Citation
Martin Bromberger, Thomas Sturm, and Christoph Weidenbach, "Linear Integer Arithmetic Revisited", in Automated Deduction -- CADE-25, edited by Amy P. Felty and Aart Middeldorp (Springer, Berlin, 2015), pp. 623-637.
Export
• Christopher W. Brown and Marek Košta, "Constructing a Single Cell in Cylindrical Algebraic Decomposition," Journal of Symbolic Computation 70, 14-48 (2015).
Citation
Christopher W. Brown and Marek Košta, "Constructing a Single Cell in Cylindrical Algebraic Decomposition," Journal of Symbolic Computation 70, 14-48 (2015).
Export
• Werner Damm, Matthias Horbach, and Viorica Sofronie-Stokkermans, "Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata", in Frontiers of Combining Systems, edited by Carsten Lutz and Silvio Ranise (Springer, Berlin, 2015), pp. 186-202.
Citation
Werner Damm, Matthias Horbach, and Viorica Sofronie-Stokkermans, "Decidability of Verification of Safety Properties of Spatial Families of Linear Hybrid Automata", in Frontiers of Combining Systems, edited by Carsten Lutz and Silvio Ranise (Springer, Berlin, 2015), pp. 186-202.
Export
• Hassan Errami, Markus Eiswirth, Dima Grigoriev, Werner M. Seiler, Thomas Sturm, and Andreas Weber, "Detection of Hopf Bifurcations in Chemical Reaction Networks Using Convex Coordinates," Journal of Computational Physics 291, 279-302 (2015).
Citation
Hassan Errami, Markus Eiswirth, Dima Grigoriev, Werner M. Seiler, Thomas Sturm, and Andreas Weber, "Detection of Hopf Bifurcations in Chemical Reaction Networks Using Convex Coordinates," Journal of Computational Physics 291, 279-302 (2015).
Export
• Pascal Fontaine, Thomas Sturm, and Uwe Waldmann, "Foreword to the Special Focus on Constraints and Combinations," Mathematics in Computer Science 9 (3), 265-265 (2015).
Citation
Pascal Fontaine, Thomas Sturm, and Uwe Waldmann, "Foreword to the Special Focus on Constraints and Combinations," Mathematics in Computer Science 9 (3), 265-265 (2015).
Export
• Willem Hagemann, Symbolic Orthogonal Projections: A New Polyhedral Representation for Reachability Analysis of Hybrid Systems, PhD Thesis, Universität des Saarlandes, 2015.
Citation
Willem Hagemann, Symbolic Orthogonal Projections: A New Polyhedral Representation for Reachability Analysis of Hybrid Systems, PhD Thesis, Universität des Saarlandes, 2015.
Export
• Maximilian Jaroschek, Pablo Federico Dobal, and Pascal Fontaine, "Adapting Real Quantifier Elimination Methods for Conflict Set Computation", in Frontiers of Combining Systems, edited by Carsten Lutz and Silvio Ranise (Springer, Berlin, 2015), pp. 151-166.
Citation
Maximilian Jaroschek, Pablo Federico Dobal, and Pascal Fontaine, "Adapting Real Quantifier Elimination Methods for Conflict Set Computation", in Frontiers of Combining Systems, edited by Carsten Lutz and Silvio Ranise (Springer, Berlin, 2015), pp. 151-166.
Export
• Christopher Junk, Robert Rößger, Georg Rock, Karsten Theis, Christoph Weidenbach, and Patrick Wischnewski, "Model-Based Variant Management with v.control", in Transdisciplinary Lifecycle Analysis of Systems, edited by Richard Curran, Nel Wognum, Milton Borsato, Josip Stiepandic, and Wim J. C. Verhagen (IOS Press, Amsterdam, 2015), pp. 194-203.
Citation
Christopher Junk, Robert Rößger, Georg Rock, Karsten Theis, Christoph Weidenbach, and Patrick Wischnewski, "Model-Based Variant Management with v.control", in Transdisciplinary Lifecycle Analysis of Systems, edited by Richard Curran, Nel Wognum, Milton Borsato, Josip Stiepandic, and Wim J. C. Verhagen (IOS Press, Amsterdam, 2015), pp. 194-203.
Export
• Manuel Kauers, Maximilian Jaroschek, and Frederik Johannson, "Ore Polynomials in Sage", in Computer Algebra and Polynomials, edited by Jaime Gutierrez, Josef Schicho, and Martin Weiman (Springer, Berlin, 2015), pp. 105-125.
Citation
Manuel Kauers, Maximilian Jaroschek, and Frederik Johannson, "Ore Polynomials in Sage", in Computer Algebra and Polynomials, edited by Jaime Gutierrez, Josef Schicho, and Martin Weiman (Springer, Berlin, 2015), pp. 105-125.
Export
• Felix Klein and Martin Zimmermann, "How Much Lookahead is Needed to Win Infinite Games?", in Automata, Languages, and Programming, edited by Magnus M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann (Springer, Berlin, 2015), pp. 452-463.
Citation
Felix Klein and Martin Zimmermann, "How Much Lookahead is Needed to Win Infinite Games?", in Automata, Languages, and Programming, edited by Magnus M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann (Springer, Berlin, 2015), pp. 452-463.
Export
• Manuel Lamotte-Schubert, Automatic Authorization Analysis, PhD Thesis, Universität des Saarlandes, 2015.
Citation
Manuel Lamotte-Schubert, Automatic Authorization Analysis, PhD Thesis, Universität des Saarlandes, 2015.
Export
• Andrew Reynolds and Jasmin Christian Blanchette, "A Decision Procedure for (Co)datatypes in SMT Solvers", in Automated Deduction -- CADE-25, edited by Amy P. Felty and Aart Middeldorp (Springer, Berlin, 2015), pp. 197-213.
Citation
Andrew Reynolds and Jasmin Christian Blanchette, "A Decision Procedure for (Co)datatypes in SMT Solvers", in Automated Deduction -- CADE-25, edited by Amy P. Felty and Aart Middeldorp (Springer, Berlin, 2015), pp. 197-213.
Export
• Renate A. Schmidt and Uwe Waldmann, "Modal Tableau Systems with Blocking and Congruence Closure", in Automated Reasoning with Analytic Tableaux and Related Methods, edited by Hans de Nivelle (Springer, Berlin, 2015), pp. 38-53.
Citation
Renate A. Schmidt and Uwe Waldmann, "Modal Tableau Systems with Blocking and Congruence Closure", in Automated Reasoning with Analytic Tableaux and Related Methods, edited by Hans de Nivelle (Springer, Berlin, 2015), pp. 38-53.
Export
• Stephan Seufert, Algorithmic Building Blocks for Relationship Analysis over Large Graphs, PhD Thesis, Universität des Saarlandes, 2015.
Citation
Stephan Seufert, Algorithmic Building Blocks for Relationship Analysis over Large Graphs, PhD Thesis, Universität des Saarlandes, 2015.
Export
• Viorica Sofronie-Stokkermans, "Hierarchical Reasoning in Local Theory Extensions and Applications", in SYNASC 2014, (IEEE Computer Society, Los Alamitos, CA, 2015), pp. 34-41.
Citation
Viorica Sofronie-Stokkermans, "Hierarchical Reasoning in Local Theory Extensions and Applications", in SYNASC 2014, (IEEE Computer Society, Los Alamitos, CA, 2015), pp. 34-41.
Export
• Thomas Sturm, "Subtropical Real Root Finding", in ISSAC'15, edited by Daniel Robertz (ACM, New York, NY, 2015), pp. 347-354.
Citation
Thomas Sturm, "Subtropical Real Root Finding", in ISSAC'15, edited by Daniel Robertz (ACM, New York, NY, 2015), pp. 347-354.
Export
• Martin Suda, "Variable and Clause Elimination for LTL Satisfiability Checking," Mathematics in Computer Science 9 (3), 327-344 (2015).
Citation
Martin Suda, "Variable and Clause Elimination for LTL Satisfiability Checking," Mathematics in Computer Science 9 (3), 327-344 (2015).
Export
• Martin Suda, Resolution-based Methods for Linear Temporal Reasoning, PhD Thesis, Universität des Saarlandes, 2015.
Citation
Martin Suda, Resolution-based Methods for Linear Temporal Reasoning, PhD Thesis, Universität des Saarlandes, 2015.
Export
• Andreas Teucke and Christoph Weidenbach, "First-order Logic Theorem Proving and Model Building via Approximation and Instantiation", in Frontiers of Combining Systems, edited by Carsten Lutz and Silvio Ranise (Springer, Berlin, 2015), pp. 85-100.
Citation
Andreas Teucke and Christoph Weidenbach, "First-order Logic Theorem Proving and Model Building via Approximation and Instantiation", in Frontiers of Combining Systems, edited by Carsten Lutz and Silvio Ranise (Springer, Berlin, 2015), pp. 85-100.
Export
• Christoph Weidenbach, "Automated Reasoning Building Blocks", in Correct System Design, edited by Roland Meyer and André Platzer (Springer, Berlin, 2015), pp. 172-188.
Citation
Christoph Weidenbach, "Automated Reasoning Building Blocks", in Correct System Design, edited by Roland Meyer and André Platzer (Springer, Berlin, 2015), pp. 172-188.
Export
• Peter Baumgartner, Joshua Bax, and Uwe Waldmann, "Finite Quantification in Hierarchic Theorem Proving", in Automated Reasoning, edited by Stephane Demri, Deepak Kapur, and Christoph Weidenbach (Springer, Berlin, 2014), pp. 152-167.
Citation
Peter Baumgartner, Joshua Bax, and Uwe Waldmann, "Finite Quantification in Hierarchic Theorem Proving", in Automated Reasoning, edited by Stephane Demri, Deepak Kapur, and Christoph Weidenbach (Springer, Berlin, 2014), pp. 152-167.
Export
• Nikolaj Bjørner, Reiner Hähnle, Tobias Nipkow, and Christoph Weidenbach (eds), Deduction and Arithmetic. (Schloss Dagstuhl, Wadern, 2014).
Citation
Nikolaj Bjørner, Reiner Hähnle, Tobias Nipkow, and Christoph Weidenbach (eds), Deduction and Arithmetic. (Schloss Dagstuhl, Wadern, 2014).
Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 13411 "Deduction and Arithmetic". The aim of this seminar was to bring together researchers working in deduction and fields related to arithmetic constraint solving. Current research in deduction can be categorized in three main strands: SMT solvers, automated first-order provers, and interactive provers. Although dealing with arithmetic has been in focus of all three for some years, there is still need of much better support of arithmetic. Reasong about arithmetic will stay at the center of attention in all three main approaches to automated deduction during the coming five to ten years. The seminar was an important event for the subcommunities involved that made it possible to communicate with each other so as to avoid duplicate effort and to exploit synergies. It succeeded also in identifying a number of important trends and open problems.
Export
• Stéphane Demri, Deepak Kapur, and Christoph Weidenbach (eds), Automated Reasoning. (Springer, Berlin, 2014).
Citation
Stéphane Demri, Deepak Kapur, and Christoph Weidenbach (eds), Automated Reasoning. (Springer, Berlin, 2014).
Export
• Arnaud Fietzke, Labelled Superposition, PhD Thesis, Universität des Saarlandes, 2014.
Citation
Arnaud Fietzke, Labelled Superposition, PhD Thesis, Universität des Saarlandes, 2014.
Export
• Silvio Ghilardi, Ulrike Sattler, and Viorica Sofronie-Stokkermans (eds), Automated Deduction: Decidability, Complexity, Tractability. (Universität Koblenz, Koblenz, 2014).
Citation
Silvio Ghilardi, Ulrike Sattler, and Viorica Sofronie-Stokkermans (eds), Automated Deduction: Decidability, Complexity, Tractability. (Universität Koblenz, Koblenz, 2014).
Export
• Matthias Horbach and Viorica Sofronie-Stokkermans, "Locality Transfer: From Constrained Axiomatizations to Reachability Predicates", in Automated Reasoning, edited by Stephane Demri, Deepak Kapur, and Christoph Weidenbach (Springer, Berlin, 2014), pp. 192-207.
Citation
Matthias Horbach and Viorica Sofronie-Stokkermans, "Locality Transfer: From Constrained Axiomatizations to Reachability Predicates", in Automated Reasoning, edited by Stephane Demri, Deepak Kapur, and Christoph Weidenbach (Springer, Berlin, 2014), pp. 192-207.
Export
• Konstantin Korovin, Marek Košta, and Thomas Sturm, "Towards Conflict-driven Learning for Virtual Substitution", in Computer Algebra in Scientific Computing, edited by Vladimir P. Gerdt, Wolfram Koepf, Werner M. Seiler, and Evgenii V. Vorozhtsov (Springer, Berlin, 2014), pp. 256-270.
Citation
Konstantin Korovin, Marek Košta, and Thomas Sturm, "Towards Conflict-driven Learning for Virtual Substitution", in Computer Algebra in Scientific Computing, edited by Vladimir P. Gerdt, Wolfram Koepf, Werner M. Seiler, and Evgenii V. Vorozhtsov (Springer, Berlin, 2014), pp. 256-270.
Abstract
We consider satisfiability modulo theory-solving for linear real arithmetic. Inspired by related work for the Fourier–Motzkin method, we combine virtual substitution with learning strategies. For the first time, we present virtual substitution—including our learning strategies—as a formal calculus. We prove soundness and completeness for that calculus. Some standard linear programming benchmarks computed with an experimental implementation of our calculus show that the integration of learning techniques into virtual substitution gives rise to considerable speedups. Our implementation is open-source and freely available.
Export
• Lei Song, Lijun Zhang, and Jens Chr. Godskesen, "Bisimulations and Logical Characterizations on Continuous-time Markov Decision Processes", in Verification, Model Checking, and Abstract Interpretation, edited by Kenneth L. McMillan and Xavier Rival (Springer, Berlin, 2014), pp. 98-117.
Citation
Lei Song, Lijun Zhang, and Jens Chr. Godskesen, "Bisimulations and Logical Characterizations on Continuous-time Markov Decision Processes", in Verification, Model Checking, and Abstract Interpretation, edited by Kenneth L. McMillan and Xavier Rival (Springer, Berlin, 2014), pp. 98-117.
Export
• Martin Suda, "Property Directed Reachability for Automated Planning," Journal of Artificial Intelligence Research 50, 265-319 (2014).
Citation
Martin Suda, "Property Directed Reachability for Automated Planning," Journal of Artificial Intelligence Research 50, 265-319 (2014).
Export
• Noran Azmy and Christoph Weidenbach, "Computing Tiny Clause Normal Forms", in Automated Deduction - CADE-24, edited by Maria Paola Bonacina (Springer, Berlin, 2013), Vol. 7898, pp. 109-125.
Citation
Noran Azmy and Christoph Weidenbach, "Computing Tiny Clause Normal Forms", in Automated Deduction - CADE-24, edited by Maria Paola Bonacina (Springer, Berlin, 2013), Vol. 7898, pp. 109-125.
Export
• Peter Baumgartner and Uwe Waldmann, "Hierarchic Superposition with Weak Abstraction", in Automated Deduction - CADE-24, edited by Maria Paola Bonacina (Springer, Berlin, 2013), pp. 39-57.
Citation
Peter Baumgartner and Uwe Waldmann, "Hierarchic Superposition with Weak Abstraction", in Automated Deduction - CADE-24, edited by Maria Paola Bonacina (Springer, Berlin, 2013), pp. 39-57.
Abstract
In this paper we study possibilities of using methods for hierarchical reasoning in local theory extensions for the analysis and verification of parametric hybrid systems, where the parameters can be either constants or functions. Our goal is to automatically provide guarantees that such systems satisfy certain safety or invariance conditions. We first analyze the possibility of automatically generating such guarantees in the form of constraints on parameters, then show that we can also synthesise so-called criticality functions, typically used for proving stability and/or safety of hybrid systems. We illustrate our methods on several examples.
Export
• Peter Baumgartner and Uwe Waldmann, "Hierarchic Superposition: Completeness without Compactness", in Proceedings of the Fifth International Conference on Mathematical Aspects of Computer and System Sciences, edited by Marek Košta and Thomas Sturm (2013), pp. 8-12.
Citation
Peter Baumgartner and Uwe Waldmann, "Hierarchic Superposition: Completeness without Compactness", in Proceedings of the Fifth International Conference on Mathematical Aspects of Computer and System Sciences, edited by Marek Košta and Thomas Sturm (2013), pp. 8-12.
Export
• Nikolaj Bjørner and Viorica Sofronie-Stokkermans, "Preface: Special Issue of Selected Extended Papers of CADE-23," Journal of Automated Reasoning 51 (1), 1-2 (2013).
Citation
Nikolaj Bjørner and Viorica Sofronie-Stokkermans, "Preface: Special Issue of Selected Extended Papers of CADE-23," Journal of Automated Reasoning 51 (1), 1-2 (2013).
Export
• Deepak Dhungana, Ching Hoo Tang, Christoph Weidenbach, and Patrick Wischnewski, "Automated Verification of Interactive Rule-based Configuration Systems", in 28th IEEE/ACM International Conference on Automated Software Engineering, edited by Ewen Denney, Tevfik Bultan, and Andreas Zeller (IEEE, Piscataway, NJ, 2013), pp. 551-561.
Citation
Deepak Dhungana, Ching Hoo Tang, Christoph Weidenbach, and Patrick Wischnewski, "Automated Verification of Interactive Rule-based Configuration Systems", in 28th IEEE/ACM International Conference on Automated Software Engineering, edited by Ewen Denney, Tevfik Bultan, and Andreas Zeller (IEEE, Piscataway, NJ, 2013), pp. 551-561.
Abstract
Rule-based specifications of systems have again become common in the context of product line variability modeling and configuration systems. In this paper, we define a logical foundation for rule-based specifications that has enough expressivity and operational behavior to be practically useful and at the same time enables decidability of important overall properties such as consistency or cycle-freeness. Our logic supports rule-based interactive user transitions as well as the definition of a domain theory via rule transitions. As a running example, we model DOPLER, a rule-based configuration system currently in use at Siemens.
Export
• Hassan Errami, Markus Eiswirth, Dima Grigoriev, Werner M. Seiler, Thomas Sturm, and Andreas Weber, "Efficient Methods to Compute Hopf Bifurcations in Chemical Reaction Networks Using Reaction Coordinates", in Computer Algebra in Scientific Computing, edited by Vladimir P. Gerdt, Wolfram Koepf, Ernst W. Mayr, and Evgenii V. Vorozhtsov (Springer, Berlin, 2013), pp. 88-99.
Citation
Hassan Errami, Markus Eiswirth, Dima Grigoriev, Werner M. Seiler, Thomas Sturm, and Andreas Weber, "Efficient Methods to Compute Hopf Bifurcations in Chemical Reaction Networks Using Reaction Coordinates", in Computer Algebra in Scientific Computing, edited by Vladimir P. Gerdt, Wolfram Koepf, Ernst W. Mayr, and Evgenii V. Vorozhtsov (Springer, Berlin, 2013), pp. 88-99.
Export
• Claudia Soa Esquivel Pinto, Computing Variable Orders for SAT-Problems, Master Thesis, Universität des Saarlandes, 2013.
Citation
Claudia Soa Esquivel Pinto, Computing Variable Orders for SAT-Problems, Master Thesis, Universität des Saarlandes, 2013.
Export
• Silvio Ghilardi, Ulrike Sattler, Viorica Sofronie-Stokkermans, and Ashish Tiwari (eds), Automated Deduction: Decidability, Complexity, Tractability. (2013).
Citation
Silvio Ghilardi, Ulrike Sattler, Viorica Sofronie-Stokkermans, and Ashish Tiwari (eds), Automated Deduction: Decidability, Complexity, Tractability. (2013).
Export
• Thomas Hillenbrand and Christoph Weidenbach, "Superposition for Bounded Domains", in Automated Reasoning and Mathematics, edited by Maria Paola Bonacina and Mark Stickel (Springer, Berlin, 2013), pp. 68-100.
Citation
Thomas Hillenbrand and Christoph Weidenbach, "Superposition for Bounded Domains", in Automated Reasoning and Mathematics, edited by Maria Paola Bonacina and Mark Stickel (Springer, Berlin, 2013), pp. 68-100.
Export
• Thomas Hillenbrand, Ruzika Piskac, Uwe Waldmann, and Christoph Weidenbach, "From Search to Computation: Redundancy Criteria and Simplification at Work", in Programming Logics, edited by Andrei Voronkov and Christoph Weidenbach (Springer, Berlin, 2013), pp. 169-193.
Citation
Thomas Hillenbrand, Ruzika Piskac, Uwe Waldmann, and Christoph Weidenbach, "From Search to Computation: Redundancy Criteria and Simplification at Work", in Programming Logics, edited by Andrei Voronkov and Christoph Weidenbach (Springer, Berlin, 2013), pp. 169-193.
Export
• Thomas Hillenbrand, Ruzica Piskac, Uwe Waldmann, and Christoph Weidenbach, "From Search to Computation: Redundancy Criteria and Simplification at Work", in Programming Logics: Essays in Memory of Harald Ganzinger, edited by Andrei Voronkov and Christoph Weidenbach (Springer, Berlin, 2013), pp. 169-193.
Citation
Thomas Hillenbrand, Ruzica Piskac, Uwe Waldmann, and Christoph Weidenbach, "From Search to Computation: Redundancy Criteria and Simplification at Work", in Programming Logics: Essays in Memory of Harald Ganzinger, edited by Andrei Voronkov and Christoph Weidenbach (Springer, Berlin, 2013), pp. 169-193.
Export
• Matthias Horbach, INFORMATIK 2013 - Informatik angepasst an Mensch, Organisation und Umwelt. (Köllen, Bonn-Buschdorf, 2013).
Citation
Matthias Horbach, INFORMATIK 2013 - Informatik angepasst an Mensch, Organisation und Umwelt. (Köllen, Bonn-Buschdorf, 2013).
Export
• Matthias Horbach and Viorica Sofronie-Stokkermans, "Obtaining Finite Local Theory Axiomatizations via Saturation", in Frontiers of Combining Systems, edited by Pascal Fontaine, Christophe Ringeissen, and Renate A. Schmidt (Springer, Berlin, 2013), pp. 198-213.
Citation
Matthias Horbach and Viorica Sofronie-Stokkermans, "Obtaining Finite Local Theory Axiomatizations via Saturation", in Frontiers of Combining Systems, edited by Pascal Fontaine, Christophe Ringeissen, and Renate A. Schmidt (Springer, Berlin, 2013), pp. 198-213.
Abstract
In this paper we present a method for obtaining local sets of clauses from possibly non-local ones. For this, we follow the work of Basin and Ganzinger and use saturation under a version of ordered resolution. In order to address the fact that saturation can generate infinite sets of clauses, we use constrained clauses and show that a link can be established between saturation and locality also for constrained clauses: This often allows us to give a finite representation of possibly infinite saturated sets of clauses.
Export
• Deepak Kapur, Robert Nieuwenhuis, Andrei Voronkov, Christoph Weidenbach, and Reinhard Wilhelm, "Harald Ganzinger's Legacy: Contributions to Logics and Programming", in Programming Logics, edited by Andrei Voronkov and Christoph Weidenbach (Springer, Berlin, 2013), pp. 1-18.
Citation
Deepak Kapur, Robert Nieuwenhuis, Andrei Voronkov, Christoph Weidenbach, and Reinhard Wilhelm, "Harald Ganzinger's Legacy: Contributions to Logics and Programming", in Programming Logics, edited by Andrei Voronkov and Christoph Weidenbach (Springer, Berlin, 2013), pp. 1-18.
Export
• Ralf Karrenberg, Marek Košta, and Thomas Sturm, "Presburger Arithmetic in Memory Access Optimization for Data-parallel Languages", in Frontiers of Combining Systems, edited by Pascal Fontaine, Christophe Ringeissen, and Renate A. Schmidt (Springer, Berlin, 2013), pp. 56-70.
Citation
Ralf Karrenberg, Marek Košta, and Thomas Sturm, "Presburger Arithmetic in Memory Access Optimization for Data-parallel Languages", in Frontiers of Combining Systems, edited by Pascal Fontaine, Christophe Ringeissen, and Renate A. Schmidt (Springer, Berlin, 2013), pp. 56-70.
Abstract
Data-parallel languages like OpenCL and CUDA are an important means to exploit the computational power of today's computing devices. We consider the compilation of such languages for CPUs with SIMD instruction sets. To generate efficient code, one wants to statically decide whether or not certain memory operations access consecutive addresses. We formalize the notion of consecutivity and algorithmically reduce the static decision to satisfiability problems in Presburger Arithmetic. We introduce a preprocessing technique on these SMT problems, which makes it feasible to apply an off-the-shelf SMT solver. We show that a prototypical OpenCL CPU driver based on our approach generates more efficient code than any other state-of-the-art driver.
Export
• Marek Košta, "SMT-based Compiler Support for Memory Access Optimization for Data-parallel Languages", in Proceedings of the Fifth International Conference on Mathematical Aspects of Computer and System Sciences, edited by Marek Košta and Thomas Sturm (2013), pp. 36-42.
Citation
Marek Košta, "SMT-based Compiler Support for Memory Access Optimization for Data-parallel Languages", in Proceedings of the Fifth International Conference on Mathematical Aspects of Computer and System Sciences, edited by Marek Košta and Thomas Sturm (2013), pp. 36-42.
Export
• Marek Košta and Thomas Sturm (eds), Proceedings of the Fifth International Conference on Mathematical Aspects of Computer and Information Sciences. (2013).
Citation
Marek Košta and Thomas Sturm (eds), Proceedings of the Fifth International Conference on Mathematical Aspects of Computer and Information Sciences. (2013).
Export
• Evgeny Kruglov, Superposition Modulo Theory, PhD Thesis, Universität des Saarlandes, 2013.
Citation
Evgeny Kruglov, Superposition Modulo Theory, PhD Thesis, Universität des Saarlandes, 2013.
Export
• Manuel Lamotte-Schubert and Christoph Weidenbach, "BDI: A New Decidable First-order Clause Class", in LPAR-19, edited by Ken McMillan, Aart Middeldorp, Geoff Sutcliffe, and Andrei Voronkov (EasyChair, Manchester, UK, 2013), pp. 62-74.
Citation
Manuel Lamotte-Schubert and Christoph Weidenbach, "BDI: A New Decidable First-order Clause Class", in LPAR-19, edited by Ken McMillan, Aart Middeldorp, Geoff Sutcliffe, and Andrei Voronkov (EasyChair, Manchester, UK, 2013), pp. 62-74.
Abstract
BDI (Bounded Depth Increase) is a new decidable first-order clause class. It strictly includes known classes such as PVD. The arity of function and predicate symbols as well as the shape of atoms is not restricted in BDI. Instead the shape of "cycles" in resolution inferences is restricted such that the depth of generated clauses may increase but is still finitely bound. The BDI class is motivated by real world problems where function terms are used to represent record structures. We show that the hyper-resolution calculus modulo redundancy elimination terminates on BDI clause sets. Employing this result to the ordered resolution calculus, we can also prove termination of ordered resolution on BDI, yielding a more efficient decision procedure.
Export
• Tianxiang Lu, Formal Verification of the Pastry Protocol, PhD Thesis, Universität des Saarlandes, 2013.
Citation
Tianxiang Lu, Formal Verification of the Pastry Protocol, PhD Thesis, Universität des Saarlandes, 2013.
Export
• Jochen Reuter, Real Linear Quantifier Elimination, Master Thesis, Universität des Saarlandes, 2013.
Citation
Jochen Reuter, Real Linear Quantifier Elimination, Master Thesis, Universität des Saarlandes, 2013.
Export
• Viorica Sofronie-Stokkermans, "Locality and Applications to Subsumption Testing in EL and Some of its Extensions," Scientific Annals of Computer Science 23 (2), 251-284 (2013).
Citation
Viorica Sofronie-Stokkermans, "Locality and Applications to Subsumption Testing in EL and Some of its Extensions," Scientific Annals of Computer Science 23 (2), 251-284 (2013).
Abstract
In this paper we show that subsumption problems in the description logics EL and EL+ can be expressed as uniform word problems in classes of semilattices with monotone operators. We use possibilities of efficient local reasoning in such classes of algebras, to obtain uniform PTIME decision procedures for TBox and CBox subsumption in EL and EL+. These locality considerations allow us to present a new family of (possibly many-sorted) logics which extend EL and EL+ with n-ary roles and/or numerical domains.
Export
• Viorica Sofronie-Stokkermans, "On Combinations of Local Theory Extensions", in Programming Logics, edited by Andrei Voronkov and Christoph Weidenbach (Springer, Berlin, 2013), pp. 392-413.
Citation
Viorica Sofronie-Stokkermans, "On Combinations of Local Theory Extensions", in Programming Logics, edited by Andrei Voronkov and Christoph Weidenbach (Springer, Berlin, 2013), pp. 392-413.
Abstract
Many problems in mathematics and computer science can be reduced to proving the satisfiability of conjunctions of literals in a background theory which is often the extension of a base theory with additional functions or a combination of theories. It is therefore important to have efficient procedures for checking satisfiability of conjunctions of ground literals in extensions and combinations of theories. For a special type of theory extensions, namely \em local extensions, hierarchic reasoning, in which a theorem prover for the base theory can be used as a black box'', is possible. Many theories used in computer science or mathematics are local extensions of a base theory. However, often it is necessary to consider complex extensions of a theory, with various types of functions. In this paper we identify situations in which a combination of local extensions of a base theory is guaranteed to be again a local extension of the base theory. We thus obtain criteria both for recognizing wider classes of local theory extensions, and for modular reasoning in combinations of theories over non-disjoint signatures.
Export
• Viorica Sofronie-Stokkermans, "Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems", in Automated Deduction - CADE-24, edited by Maria Paola Bonacina (Springer, Berlin, 2013), pp. 360-376.
Citation
Viorica Sofronie-Stokkermans, "Hierarchical Reasoning and Model Generation for the Verification of Parametric Hybrid Systems", in Automated Deduction - CADE-24, edited by Maria Paola Bonacina (Springer, Berlin, 2013), pp. 360-376.
Abstract
In this paper we study possibilities of using methods for hierarchical reasoning in local theory extensions for the analysis and verification of parametric hybrid systems, where the parameters can be either constants or functions. Our goal is to automatically provide guarantees that such systems satisfy certain safety or invariance conditions. We first analyze the possibility of automatically generating such guarantees in the form of constraints on parameters, then show that we can also synthesise so-called criticality functions, typically used for proving stability and/or safety of hybrid systems. We illustrate our methods on several examples.
Export
• Martin Suda, "Variable and Clause Elimination for LTL Satisfiability Checking", in Proceedings of the Fifth International Conference on Mathematical Aspects of Computer and System Sciences, edited by Marek Košta and Thomas Sturm (2013), pp. 60-74.
Citation
Martin Suda, "Variable and Clause Elimination for LTL Satisfiability Checking", in Proceedings of the Fifth International Conference on Mathematical Aspects of Computer and System Sciences, edited by Marek Košta and Thomas Sturm (2013), pp. 60-74.
Export
• Andreas Teucke, CDCL with Reduction, Master Thesis, Universität des Saarlandes, 2013.
Citation
Andreas Teucke, CDCL with Reduction, Master Thesis, Universität des Saarlandes, 2013.
Export
• Andrei Voronkov and Christoph Weidenbach (eds), Programming Logics. (Springer, Berlin, 2013).
Citation
Andrei Voronkov and Christoph Weidenbach (eds), Programming Logics. (Springer, Berlin, 2013).
Export
• Noran Azmy, Formula Renaming with Generalizations, Master Thesis, Universität des Saarlandes, 2012.
Citation
Noran Azmy, Formula Renaming with Generalizations, Master Thesis, Universität des Saarlandes, 2012.
Export
• Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, and Christoph Weidenbach, "More SPASS with Isabelle: Superposition with Hard Sorts and Configurable Simplification", in Interactive Theorem Proving, edited by Lennart Beringer and Amy Felty (Springer, Berlin, 2012), pp. 345-360.
Citation
Jasmin Christian Blanchette, Andrei Popescu, Daniel Wand, and Christoph Weidenbach, "More SPASS with Isabelle: Superposition with Hard Sorts and Configurable Simplification", in Interactive Theorem Proving, edited by Lennart Beringer and Amy Felty (Springer, Berlin, 2012), pp. 345-360.
Export
• Martin Bromberger, Adapting the Simplex Algorithm for Superposition Modulo Linear Arithmetic, Bachelor Thesis, Universität des Saarlandes, 2012.
Citation
Martin Bromberger, Adapting the Simplex Algorithm for Superposition Modulo Linear Arithmetic, Bachelor Thesis, Universität des Saarlandes, 2012.
Export
• Werner Damm, Henning Dierks, Stefan Disch, Willem Hagemann, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, and Boris Wirtz, "Exact and Fully Symbolic Verification of Linear Hybrid Automata with Large Discrete State Spaces," Science of Computer Programming 77, 1122-1150 (2012).
Citation
Werner Damm, Henning Dierks, Stefan Disch, Willem Hagemann, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, and Boris Wirtz, "Exact and Fully Symbolic Verification of Linear Hybrid Automata with Large Discrete State Spaces," Science of Computer Programming 77, 1122-1150 (2012).
Export
• Arnaud Fietzke, Evgeny Kruglov, and Christoph Weidenbach, "Automatic Generation of Invariants for Circular Derivations in SUP(LA)", in Logic for Programming, Artificial Intelligence, and Reasoning, edited by Nikolaj Bjørner and Andrei Voronkov (Springer, Berlin, 2012), pp. 197-211.
Citation
Arnaud Fietzke, Evgeny Kruglov, and Christoph Weidenbach, "Automatic Generation of Invariants for Circular Derivations in SUP(LA)", in Logic for Programming, Artificial Intelligence, and Reasoning, edited by Nikolaj Bjørner and Andrei Voronkov (Springer, Berlin, 2012), pp. 197-211.
Abstract
The hierarchic combination of linear arithmetic and firstorder logic with free function symbols, FOL(LA), results in a strictly more expressive logic than its two parts. The SUP(LA) calculus can be turned into a decision procedure for interesting fragments of FOL(LA). For example, reachability problems for timed automata can be decided by SUP(LA) using an appropriate translation into FOL(LA). In this paper, we extend the SUP(LA) calculus with an additional inference rule, automatically generating inductive invariants from partial SUP(LA) derivations. The rule enables decidability of more expressive fragments, including reachability for timed automata with unbounded integer variables. We have implemented the rule in the SPASS(LA) theorem prover with promising results, showing that it can considerably speed up proof search and enable termination of saturation for practically relevant problems.
Export
• Pascal Fontaine, Stephan Merz, and Christoph Weidenbach, "Combination of Disjoint Theories: Beyond Decidability", in Automated Reasoning, edited by Bernhard Gramlich and Dale Miller (Springer, Berlin, 2012), pp. 256-270.
Citation
Pascal Fontaine, Stephan Merz, and Christoph Weidenbach, "Combination of Disjoint Theories: Beyond Decidability", in Automated Reasoning, edited by Bernhard Gramlich and Dale Miller (Springer, Berlin, 2012), pp. 256-270.
Export
• Evgeny Kruglov and Christoph Weidenbach, "Superposition Decides the First-order Logic Fragment Over Ground Theories," Mathematics in Computer Science 6 (4), 427-456 (2012).
Citation
Evgeny Kruglov and Christoph Weidenbach, "Superposition Decides the First-order Logic Fragment Over Ground Theories," Mathematics in Computer Science 6 (4), 427-456 (2012).
Abstract
The hierarchic superposition calculus over a theory T, called SUP(T), enables sound reasoning on the hierarchic combination of a theory T with full first-order logic, FOL(T). If a FOL(T) clause set enjoys a sufficient completeness criterion, the calculus is even complete. Clause sets over the ground fragment of FOL(T) are not sufficiently complete, in general. In this paper we show that any clause set over the ground FOL(T) fragment can be transformed into a sufficiently complete one, and prove that SUP(T) terminates on the transformed clause set, hence constitutes a decision procedure provided the existential fragment of the theory T is decidable. Thanks to the hierarchic design of SUP(T), the decidability result can be extended beyond the ground case. We show SUP(T) is a decision procedure for the non-ground FOL fragment plus a theory T, if every non-constant function symbol from the underlying FOL signature ranges into the sort of the theory T, and every term of the theory sort is ground. Examples for T are in particular decidable fragments of arithmetic.
Export
• Nicolas Peltier and Viorica Sofronie-Stokkermans, "First-order Theorem Proving: Foreword," Journal of Symbolic Computation 47 (9), 1009-1010 (2012).
Citation
Nicolas Peltier and Viorica Sofronie-Stokkermans, "First-order Theorem Proving: Foreword," Journal of Symbolic Computation 47 (9), 1009-1010 (2012).
Export
• Martin Suda and Christoph Weidenbach, "Labelled Superposition for PLTL", in Logic for Programming, Artificial Intelligence, and Reasoning, edited by Nikolaj Bjørner and Andrei Voronkov (Springer, Berlin, 2012), pp. 391-405.
Citation
Martin Suda and Christoph Weidenbach, "Labelled Superposition for PLTL", in Logic for Programming, Artificial Intelligence, and Reasoning, edited by Nikolaj Bjørner and Andrei Voronkov (Springer, Berlin, 2012), pp. 391-405.
Abstract
This paper introduces a new decision procedure for PLTL based on labelled superposition. Its main idea is to treat temporal formulas as infinite sets of purely propositional clauses over an extended signature. These infinite sets are then represented by finite sets of labelled propositional clauses. The new representation enables the replacement of the complex temporal resolution rule, suggested by existing resolution calculi for PLTL, by a fine grained repetition check of finitely saturated labelled clause sets followed by a simple inference. The completeness argument is based on the standard model building idea from superposition. It inherently justifies ordering restrictions, redundancy elimination and effective partial model building. The latter can be directly used to effectively generate counterexamples of non-valid PLTL conjectures out of saturated labelled clause sets in a straightforward way.
Export
• Martin Suda and Christoph Weidenbach, "A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance", in Automated Reasoning, edited by Bernhard Gramlich, Dale Miller, and Uli Sattler (Springer, Berlin, 2012), pp. 537-543.
Citation
Martin Suda and Christoph Weidenbach, "A PLTL-Prover Based on Labelled Superposition with Partial Model Guidance", in Automated Reasoning, edited by Bernhard Gramlich, Dale Miller, and Uli Sattler (Springer, Berlin, 2012), pp. 537-543.
Abstract
Labelled superposition (LPSup) is a new calculus for PLTL. One of its distinguishing features, in comparison to other resolution-based approaches, is its ability to construct partial models on the fly. We use this feature to design a new decision procedure for the logic, where the models are effectively used to guide the search. On a representative set of benchmarks, our implementation is then shown to considerably advance the state of the art.
Export
• Patrick Wischnewski, Efficient Reasoning Procedures for Complex First-order Theories, PhD Thesis, Universität des Saarlandes, 2012.
Citation
Patrick Wischnewski, Efficient Reasoning Procedures for Complex First-order Theories, PhD Thesis, Universität des Saarlandes, 2012.
Export
• Peter Baumgartner and Uwe Waldmann, "A Combined Superposition and Model Evolution Calculus," Journal of Automated Reasoning 47 (2), 191-227 (2011).
Citation
Peter Baumgartner and Uwe Waldmann, "A Combined Superposition and Model Evolution Calculus," Journal of Automated Reasoning 47 (2), 191-227 (2011).
Abstract
We present a new calculus for first-order theorem proving with equality, ME+Sup, which generalizes both the Superposition calculus and the Model Evolution calculus (with equality) by integrating their inference rules and redundancy criteria in a non-trivial way. The main motivation is to combine the advantageous features of these two rather complementary calculi in a single framework. In particular, Model Evolution, as a lifted version of the propositional DPLL procedure, contributes a non-ground splitting rule that effectively permits to split a clause into \emph{non} variable disjoint subclauses. In the paper we present the calculus in detail. Our main result is its completeness under semantically justified redundancy criteria and simplification rules. We also show how under certain assumptions the model representation computed by a (finite and fair) derivation can be queried in an effective way.
Export
• Nikolaj Bjørner and Viorica Sofronie-Stokkermans (eds), Automated Deduction - CADE-23: 23rd International Conference on Automated Deduction. (Springer, Berlin, 2011).
Citation
Nikolaj Bjørner and Viorica Sofronie-Stokkermans (eds), Automated Deduction - CADE-23: 23rd International Conference on Automated Deduction. (Springer, Berlin, 2011).
Export
• Guillaume Burel, "Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo," Logical Methods in Computer Science 7 (1), 3 (2011).
Citation
Guillaume Burel, "Efficiently Simulating Higher-Order Arithmetic by a First-Order Theory Modulo," Logical Methods in Computer Science 7 (1), 3 (2011).
Abstract
In deduction modulo, a theory is not represented by a set of axioms but by a congruence on propositions modulo which the inference rules of standard deductive systems---such as for instance natural deduction---are applied. Therefore, the reasoning that is intrinsic of the theory does not appear in the length of proofs. In general, the congruence is defined through a rewrite system over terms and propositions. We define a rigorous framework to study proof lengths in deduction modulo, where the congruence must be computed in polynomial time. We show that even very simple rewrite systems lead to arbitrary proof-length speed-ups in deduction modulo, compared to using axioms. As higher-order logic can be encoded as a first-order theory in deduction modulo, we also study how to reinterpret, thanks to deduction modulo, the speed-ups between higher-order and first-order arithmetics that were stated by G\"odel. We define a first-order rewrite system with a congruence decidable in polynomial time such that proofs of higher-order arithmetic can be linearly translated into first-order arithmetic modulo that system. We also present the whole higher-order arithmetic as a first-order system without resorting to any axiom, where proofs have the same length as in the axiomatic presentation.
Export
• Werner Damm, Carsten Ihlemann, and Viorica Sofronie-Stokkermans, "PTIME parametric verification of safety properties for reasonable linear hybrid automata," Mathematics in Computer Science 5 (4), 469-497 (2011).
Citation
Werner Damm, Carsten Ihlemann, and Viorica Sofronie-Stokkermans, "PTIME parametric verification of safety properties for reasonable linear hybrid automata," Mathematics in Computer Science 5 (4), 469-497 (2011).
Abstract
This paper identifies an industrially relevant class of linear hybrid automata (LHA) called reasonable LHA for which parametric verification of convex safety properties with exhaustive entry states can be verified in polynomial time and time-bounded reachability can be decided in nondeterministic polynomial time for non-parametric verification and in exponential time for parametric verification. Properties with exhaustive entry states are restricted to runs originating in a (specified) inner envelope of some mode-invariant. Deciding whether an LHA is reasonable is shown to be decidable in polynomial time.
Export
• Werner Damm, Carsten Ihlemann, and Viorica Sofronie-Stokkermans, "Decidability and complexity for the verification of safety properties of reasonable linear hybrid automata", in HSCC’11: Proceedings of the 2011 ACM/SIGBED Hybrid Systems: Computation and Control, edited by Emilio Frazzoli and Radu Grosu (ACM, New York, NY, 2011), pp. 73-82.
Citation
Werner Damm, Carsten Ihlemann, and Viorica Sofronie-Stokkermans, "Decidability and complexity for the verification of safety properties of reasonable linear hybrid automata", in HSCC’11: Proceedings of the 2011 ACM/SIGBED Hybrid Systems: Computation and Control, edited by Emilio Frazzoli and Radu Grosu (ACM, New York, NY, 2011), pp. 73-82.
Abstract
We study linear hybrid automata with dynamics of the form $\sum a_i x_i \leq a$ and $\sum b_i {\dot x_i} \leq b$. We show that verification of safety properties for reasonable classes of such systems can be reduced to invariant checking and bounded model checking and, ultimately, to checking the validity of certain formulae (obtained using a polynomial reduction). We show that the problem of checking the validity of the formulae obtained this way is typically in NP, and identify verification tasks which can be performed in PTIME. These reductions can also be used for parametric systems, both for checking safety properties given constraints on parameters, and for deriving constraints of parameters that guarantee that safety properties hold.
Export
• Werner Damm, Carsten Ihlemann, and Viorica Sofronie-Stokkermans, "PTIME Parametric Verification of Safety Properties for Reasonable Linear Hybrid Automata", in AVACS Technical Report, (2011), Vol. 70, pp. 31 p.
Citation
Werner Damm, Carsten Ihlemann, and Viorica Sofronie-Stokkermans, "PTIME Parametric Verification of Safety Properties for Reasonable Linear Hybrid Automata", in AVACS Technical Report, (2011), Vol. 70, pp. 31 p.
Abstract
This paper identifies an industrially relevant class of linear hybrid automata (LHA) called reasonable LHA for which parametric verification of convex safety properties with exhaustive entry states can be verified in polynomial time and time-bounded reachability can be decided in nondeterministic polynomial time for non-parametric verification and in exponential time for parametric verification. Properties with exhaustive entry states are restricted to runs originating in a (specified) inner envelope of some mode-invariant. Deciding whether an LHA is reasonable is shown to be decidable in polynomial time.
Export
• Werner Damm, Stefan Disch, Willem Hagemann, Christoph Scholl, Uwe Waldmann, and Boris Wirtz, "Integrating Incremental Flow Pipes into a Symbolic Model Checker for Hybrid Systems", in AVACS Technical Report, (2011), Vol. 76.
Citation
Werner Damm, Stefan Disch, Willem Hagemann, Christoph Scholl, Uwe Waldmann, and Boris Wirtz, "Integrating Incremental Flow Pipes into a Symbolic Model Checker for Hybrid Systems", in AVACS Technical Report, (2011), Vol. 76.
Abstract
We describe an approach to integrate incremental ow pipe computation into a fully symbolic backward model checker for hybrid systems. Our method combines the advantages of symbolic state set representation, such as the ability to deal with large numbers of boolean variables, with an effcient way to handle continuous ows dened by linear differential equations, possibly including bounded disturbances.
Export
• Andreas Eggers, Evgeny Kruglov, Stefan Kupferschmid, Karsten Scheibler, Teige Teige, and Christoph Weidenbach, "Superposition Modulo Non-linear Arithmetic", in Frontiers of Combining Systems, edited by Viorica Sofronie-Stokkermans and Cesare Tinelli (Springer, Berlin, 2011), pp. 119-134.
Citation
Andreas Eggers, Evgeny Kruglov, Stefan Kupferschmid, Karsten Scheibler, Teige Teige, and Christoph Weidenbach, "Superposition Modulo Non-linear Arithmetic", in Frontiers of Combining Systems, edited by Viorica Sofronie-Stokkermans and Cesare Tinelli (Springer, Berlin, 2011), pp. 119-134.
Abstract
The first-order theory over non-linear arithmetic including transcendental functions (NLA) is undecidable. Nevertheless, in this paper we show that a particular combination with superposition leads to a sound and complete calculus that is useful in practice. We follow basically the ideas of the SUP(LA) combination, but have to take care of undecidability, resulting in unknown'' answers by the NLA reasoning procedure. A pipeline of NLA constraint simplification techniques related to the SUP(NLA) framework significantly decreases the number of unknown'' answers. The resulting approach is implemented as SUP(NLA) by a system combination of SPASS and iSAT. Applied to various scenarios of traffic collision avoidance protocols, we show by experiments that SPASS(iSAT) can fully automatically proof and disproof safety properties of such protocols using the very same formalization.
Export
• Francis Gasse and Viorica Sofronie-Stokkermans, "Efficient TBox Subsumption Checking in Combinations of EL and (fragments of) FL0", in Proceedings of the 2011 International Workshop on Description Logics (DL-2011), edited by Riccardo Rosati, Sebastian Rudolph, and Michael Zakharyaschev (CEUR Workshop Proceedings, Aachen, Germany, 2011), pp. 125-135.
Citation
Francis Gasse and Viorica Sofronie-Stokkermans, "Efficient TBox Subsumption Checking in Combinations of EL and (fragments of) FL0", in Proceedings of the 2011 International Workshop on Description Logics (DL-2011), edited by Riccardo Rosati, Sebastian Rudolph, and Michael Zakharyaschev (CEUR Workshop Proceedings, Aachen, Germany, 2011), pp. 125-135.
Abstract
We study possibilities of combining (fragments) of the lightweight description logics ${\cal F}{\cal L}_0$ and ${\cal E}{\cal L}$, and identify classes of subsumption problems in a combination of ${\cal E}{\cal L}$ and Horn-${\cal F}{\cal L}_0$, which can be checked in PSPACE resp. PTIME. Since ${\cal F}{\cal L}_0$ allows universal role restrictions and ${\cal E}{\cal L}$ allows existential role restrictions, we thus have a framework where subsumption between expressions including both types of role restrictions (but for disjoint sets of roles) can be checked in polynomial space or time.
Export
• Aless Lasaruk and Thomas Sturm, "Automatic Verification of the Adequacy of Models for Families of Geometric Objects", in Automated Deduction in Geometry, edited by Thomas Sturm and Christoph Zengler (Springer, Berlin, 2011), pp. 116-140.
Citation
Aless Lasaruk and Thomas Sturm, "Automatic Verification of the Adequacy of Models for Families of Geometric Objects", in Automated Deduction in Geometry, edited by Thomas Sturm and Christoph Zengler (Springer, Berlin, 2011), pp. 116-140.
Abstract
We consider parametric families of semi-algebraic geometric objects, each implicitly defined by a first-order formula. Given an unambiguous description of such an object family and an intended alternative description we automatically construct a first-order formula which is true if and only if our alternative description uniquely describes geometric objects of the reference description. We can decide this formula by applying real quantifier elimination. In the positive case we furthermore derive the defining first-order formulas corresponding to our new description. In the negative case we can produce sample points establishing a counterexample for the uniqueness. We demonstrate our method by automatically proving uniqueness theorems for characterizations of several geometric primitives and simple complex objects. Finally, we focus on tori, characterizations of which can be applied in spline approximation theory with toric segments. Although we cannot yet practically solve the fundamental open questions in this area within reasonable time and space, we demonstrate that they can be formulated in our framework. In addition this points at an interesting and practically relevant challenge problem for automated deduction in geometry in general.
Export
• Tianxiang Lu, Stephan Merz, and Christoph Weidenbach, "Towards Verification of the Pastry Protocol using TLA+", in Research Report, (2011), pp. 51 p.
Citation
Tianxiang Lu, Stephan Merz, and Christoph Weidenbach, "Towards Verification of the Pastry Protocol using TLA+", in Research Report, (2011), pp. 51 p.
Abstract
Pastry is an algorithm that provides a scalable distributed hash table over an underlying P2P network. Several implementations of Pastry are available and have been applied in practice, but no attempt has so far been made to formally describe the algorithm or to verify its properties. Since Pastry combines rather complex data structures, asynchronous communication, concurrency, resilience to churn and fault tolerance, it makes an interesting target for verication. We have modeled Pastry's core routing algorithms and communication protocol in the specication language TLA+. In order to validate the model and to search for bugs we employed the TLA+ model checker tlc to analyze several qualitative properties. We obtained non-trivial insights in the behavior of Pastry through the model checking analysis. Furthermore, we started to verify Pastry using the very same model and the interactive theorem prover tlaps for TLA+. A rst result is the reduction of global Pastry correctness properties to invariants of the underlying data structures.
Export
• Tianxiang Lu, Stephan Merz, and Christoph Weidenbach, "Towards Verification of the Pastry Routing Protocol using TLA+", in Formal Techniques for Distributed Systems, edited by Roberto Bruni and Juergen Dingel (Springer, Berlin, 2011), pp. 244-258.
Citation
Tianxiang Lu, Stephan Merz, and Christoph Weidenbach, "Towards Verification of the Pastry Routing Protocol using TLA+", in Formal Techniques for Distributed Systems, edited by Roberto Bruni and Juergen Dingel (Springer, Berlin, 2011), pp. 244-258.
Export
• Thomas Sturm and Christoph Zengler (eds), Automated Deduction in Geometry: 7th International Workshop, ADG 2008. (Springer, Berlin, 2011).
Citation
Thomas Sturm and Christoph Zengler (eds), Automated Deduction in Geometry: 7th International Workshop, ADG 2008. (Springer, Berlin, 2011).
Export
• Thomas Sturm and Ashish Tiwari, "Verification and Synthesis Using Real Quantifier Elimination", in ISSAC 2011, edited by Anton Leykin (ACM, New York, NY, 2011), pp. 329-336.
Citation
Thomas Sturm and Ashish Tiwari, "Verification and Synthesis Using Real Quantifier Elimination", in ISSAC 2011, edited by Anton Leykin (ACM, New York, NY, 2011), pp. 329-336.
Abstract
We present the application of real quantifier elimination to formal verification and synthesis of continuous and switched dynamical systems. Through a series of case studies, we show how first-order formulas over the reals arise when formally analyzing models of complex control systems. Existing off-the-shelf quantifier elimination procedures are not successful in eliminating quantifiers from many of our benchmarks. We therefore automatically combine three established software components: virtual subtitution based quantifier elimination in Reduce/Redlog, cylindrical algebraic decomposition implemented in Qepcad, and the simplifier Slfq implemented on top of Qepcad. We use this combination to successfully analyze various models of systems including adaptive cruise control in automobiles, adaptive flight control system, and the classical inverted pendulum problem studied in control theory.
Export
• Cesare Tinelli and Viorica Sofronie-Stokkermans (eds), Frontiers of Combining Systems. (Springer, Berlin, 2011).
Citation
Cesare Tinelli and Viorica Sofronie-Stokkermans (eds), Frontiers of Combining Systems. (Springer, Berlin, 2011).
Export
• Andreas Weber, Thomas Sturm, and Essam O. Abdel-Rahman, "Algorithmic Global Criteria for Excluding Oscillations," Bulletin of Mathematical Biology 73 (4), 899-916 (2011).
Citation
Andreas Weber, Thomas Sturm, and Essam O. Abdel-Rahman, "Algorithmic Global Criteria for Excluding Oscillations," Bulletin of Mathematical Biology 73 (4), 899-916 (2011).
Abstract
We investigate algorithmic methods to tackle the following problem: Given a system of parametric ordinary differential equations built by a biological model, does there exist ranges of values for the model parameters and variables which are both meaningful from a biological point of view and where oscillating trajectories, can be found? We show that in the common case of polynomial vector fields known criteria excluding the existence of non-constant limit cycles lead to quantifier elimination problems over the reals. We apply these criteria to various models that have been previously investigated in the context of algebraic biology.
Export
• Guillaume Burel, "Embedding Deduction Modulo into a Prover", in Computer Science Logic, edited by Anuj Dawar and Helmut Veith (Springer, Berlin, 2010), pp. 155-169.
Citation
Guillaume Burel, "Embedding Deduction Modulo into a Prover", in Computer Science Logic, edited by Anuj Dawar and Helmut Veith (Springer, Berlin, 2010), pp. 155-169.
Abstract
Deduction modulo consists in presenting a theory through rewrite rules to support automatic and interactive proof search. It induces proof search methods based on narrowing, such as the polarized resolution modulo. We show how to combine this method with more traditional ordering restrictions. Interestingly, no compatibility between the rewriting and the ordering is requested to ensure completeness. We also show that some simplification rules, such as strict subsumption eliminations and demodulations, preserve completeness. For this purpose, we use a new framework based on a proof ordering. These results show that polarized resolution modulo can be integrated into existing provers, where these restrictions and simplifications are present. We also discuss how this integration can actually be done by diverting the main algorithm of state-of-the-art provers.
Export
• Johannes Faber, Carsten Ihlemann, Swen Jacobs, and Viorica Sofronie-Stokkermans, "Automatic Verification of Parametric Specifications with Complex Topologies", in Integrated Formal Methods, edited by Dominique Mery and Stephan Merz (Springer, Berlin, 2010), pp. 152-167.
Citation
Johannes Faber, Carsten Ihlemann, Swen Jacobs, and Viorica Sofronie-Stokkermans, "Automatic Verification of Parametric Specifications with Complex Topologies", in Integrated Formal Methods, edited by Dominique Mery and Stephan Merz (Springer, Berlin, 2010), pp. 152-167.
Abstract
The focus of this paper is on reducing the complexity in verification by exploiting modularity at various levels: in specification, in verification, and structurally. \begin{itemize} \item For specifications, we use the modular language CSP-OZ-DC, which allows us to decouple verification tasks concerning data from those concerning durations. \item At the verification level, we exploit modularity in theorem proving for rich data structures and use this for invariant checking. \item At the structural level, we analyze possibilities for modular verification of systems consisting of various components which interact. \end{itemize} We illustrate these ideas by automatically verifying safety properties of a case study from the European Train Control System standard, which extends previous examples by comprising a complex track topology with lists of track segments and trains with different routes.
Export
• Johannes Faber, Carsten Ihlemann, Swen Jacobs, and Viorica Sofronie-Stokkermans, "Automatic Verification of Parametric Specifications with Complex Topologies", in AVACS Technical Report, (2010), Vol. 66, pp. 40 p.
Citation
Johannes Faber, Carsten Ihlemann, Swen Jacobs, and Viorica Sofronie-Stokkermans, "Automatic Verification of Parametric Specifications with Complex Topologies", in AVACS Technical Report, (2010), Vol. 66, pp. 40 p.
Abstract
The focus of this paper is on reducing the complexity in verification by exploiting modularity at various levels: in specification, in verification, and structurally. \begin{itemize} \item For specifications, we use the modular language CSP-OZ-DC, which allows us to decouple verification tasks concerning data from those concerning durations. \item At the verification level, we exploit modularity in theorem proving for rich data structures and use this for invariant checking. \item At the structural level, we analyze possibilities for modular verification of systems consisting of various components which interact. \end{itemize} We illustrate these ideas by automatically verifying safety properties of a case study from the European Train Control System standard, which extends previous examples by comprising a complex track topology with lists of track segments and trains with different routes.
Export
• Arnaud Fietzke, Holger Hermanns, and Christoph Weidenbach, "Superposition-Based Analysis of First-Order Probabilistic Timed Automata", in Logic for Programming, Artificial Intelligence, and Reasoning, edited by Christian G. Fermüller and Andrei Voronkov (Springer, Berlin, 2010), pp. 302-316.
Citation
Arnaud Fietzke, Holger Hermanns, and Christoph Weidenbach, "Superposition-Based Analysis of First-Order Probabilistic Timed Automata", in Logic for Programming, Artificial Intelligence, and Reasoning, edited by Christian G. Fermüller and Andrei Voronkov (Springer, Berlin, 2010), pp. 302-316.
Abstract
This paper discusses the analysis of first-order probabilistic timed automata (FPTA) by a combination of hierarchic first-order superposition-based theorem proving and probabilistic model checking. We develop the overall semantics of FPTAs and prove soundness and completeness of our method for reachability properties. Basically, we decompose FPTAs into their time plus first-order logic aspects on the one hand, and their probabilistic aspects on the other hand. Then we exploit the time plus first-order behavior by hierarchic superposition over linear arithmetic. The result of this analysis is the basis for the construction of a reachability equivalent (to the original FPTA) probabilistic timed automaton to which probabilistic model checking is finally applied. The hierarchic superposition calculus required for the analysis is sound and complete on the first-order formulas generated from FPTAs. It even works well in practice. We illustrate the potential behind it with a real-life DHCP protocol example, which we analyze by means of tool chain support.
Export
• Silvio Ghilardi, Ulrike Sattler, Viorica Sofronie-Stokkermans, and Ashish Tiwari, "Special Issue on Automated Deduction: Decidability, complexity, tractability," Journal of Symbolic Computation 45 (2), - (2010).
Citation
Silvio Ghilardi, Ulrike Sattler, Viorica Sofronie-Stokkermans, and Ashish Tiwari, "Special Issue on Automated Deduction: Decidability, complexity, tractability," Journal of Symbolic Computation 45 (2), - (2010).
Export
• Matthias Horbach and Christoph Weidenbach, "Superposition for Fixed Domains," ACM Transactions on Computational Logic 11 (4), 27 (2010).
Citation
Matthias Horbach and Christoph Weidenbach, "Superposition for Fixed Domains," ACM Transactions on Computational Logic 11 (4), 27 (2010).
Abstract
Disunification is an extension of unification to first-order formulae over syntactic equality atoms. Instead of considering only syntactic equality, I extend a disunification algorithm by Comon and Delor to ultimately periodic interpretations, i.e.~minimal many-sorted Herbrand models of predicative Horn clauses and, for some sorts, equations of the form $s^\upmb(x)\eq s^\upma(x)$. The extended algorithm is terminating and correct for ultimately periodic interpretations over a finite signature and gives rise to a decision procedure for the satisfiability of equational formulae in ultimately periodic interpretations. As an application, I show how to apply disunification to compute the completion of predicates with respect to an ultimately periodic interpretation. Such completions are a key ingredient to several inductionless induction methods.
Export
• Matthias Horbach, "Disunification for Ultimately Periodic Interpretations", in Logic for Programming, Artificial Intelligence, and Reasoning, edited by Edmund M. Clarke and Andrei Voronkov (Springer, Berlin, 2010), pp. 290-311.
Citation
Matthias Horbach, "Disunification for Ultimately Periodic Interpretations", in Logic for Programming, Artificial Intelligence, and Reasoning, edited by Edmund M. Clarke and Andrei Voronkov (Springer, Berlin, 2010), pp. 290-311.
Export
• Matthias Horbach, Saturation-based Decision Procedures for Fixed Domain and Minimal Model Semantics, PhD Thesis, Universität des Saarlandes, 2010.
Citation
Matthias Horbach, Saturation-based Decision Procedures for Fixed Domain and Minimal Model Semantics, PhD Thesis, Universität des Saarlandes, 2010.
Abstract
Superposition is an established decision procedure for a variety of first-order logic theories represented by sets of clauses. A satisfiable theory, saturated by superposition, implicitly defines a minimal Herbrand model for the theory. This raises the question in how far superposition calculi can be employed for reasoning about such minimal models. This is indeed often possible when existential properties are considered. However, proving universal properties directly leads to a modification of the minimal model's term-generated domain, as new Skolem functions are introduced. For many applications, this is not desired because it changes the problem. In this thesis, I propose the first superposition calculus that can explicitly represent existentially quantified variables and can thus compute with respect to a given fixed domain. It does not eliminate existential variables by Skolemization, but handles them using additional constraints with which each clause is annotated. This calculus is sound and refutationally complete in the limit for a fixed domain semantics. For saturated Horn theories and classes of positive formulas, the calculus is even complete for proving properties of the minimal model itself, going beyond the scope of known superposition-based approaches. The calculus is applicable to every set of clauses with equality and does not rely on any syntactic restrictions of the input. Extensions of the calculus lead to various new decision procedures for minimal model validity. A main feature of these decision procedures is that even the validity of queries containing one quantifier alternation can be decided. In particular, I prove that the validity of any formula with at most one quantifier alternation is decidable in models represented by a finite set of atoms and that the validity of several classes of such formulas is decidable in models represented by so-called disjunctions of implicit generalizations. Moreover, I show that the decision of minimal model validity can be reduced to the superposition-based decision of first-order validity for models of a class of predicative Horn clauses where all function symbols are at most unary.
Export
• Carsten Ihlemann and Viorica Sofronie-Stokkermans, "On Hierarchical Reasoning in Combinations of Theories", in Automated Reasoning, edited by Jürgen Giesl and Reiner Hähnle (Springer, Berlin, 2010), pp. 30-45.
Citation
Carsten Ihlemann and Viorica Sofronie-Stokkermans, "On Hierarchical Reasoning in Combinations of Theories", in Automated Reasoning, edited by Jürgen Giesl and Reiner Hähnle (Springer, Berlin, 2010), pp. 30-45.
Abstract
In this paper we study theory combinations over non-disjoint signatures in which hierarchical and modular reasoning is possible. We use a notion of locality of a theory extension parameterized by a closure operator on ground terms. We give criteria for recognizing these types of theory extensions. We then show that combinations of extensions of theories which are local in this extended sense also have a locality property and hence allow modular and hierarchical reasoning. We thus obtain parameterized decidability and complexity results for many (combinations of) theories important in verification.
Export
• Carsten Ihlemann, Reasoning in Combinations of Theories, PhD Thesis, Universität des Saarlandes, 2010.
Citation
Carsten Ihlemann, Reasoning in Combinations of Theories, PhD Thesis, Universität des Saarlandes, 2010.
Abstract
Verification problems are often expressed in a language which mixes several theories. A natural question to ask is whether one can use decision procedures for individual theories to construct a decision procedure for the union theory. In the cases where this is possible one has a powerful method at hand to handle complex theories effectively. The setup considered in this thesis is that of one base theory which is extended by one or more theories. The question is if and when a given ground satisfiability problem in the extended setting can be effectively reduced to an equi-satisfiable problem over the base theory. A case where this reductive approach is always possible is that of so-called \emph{local theory extensions.} The theory of local extensions is developed and some applications concerning monotone functions are given. Then the theory of local theory extensions is generalized in order to deal with data structures that exhibit local behavior. It will be shown that a suitable fragment of both the theory of arrays and the theory of pointers is local in this broader sense. % Finally, the case of more than one theory extension is discussed. In particular, a \emph{modularity} result is given that under certain circumstances the locality of each of the extensions lifts to locality of the entire extension. The reductive approach outlined above has become particularly relevant in recent years due to the rise of powerful solvers for background theories common in verification tasks. These so-called SMT-solvers effectively handle theories such as real linear or integer arithmetic. As part of this thesis, a program called \emph{\mbox{H-PILoT}} was implemented which carries out reductive reasoning for local theory extensions. H-PILoT found applications in mathematics, multiple-valued logics, data-structures and reasoning in complex systems.
Export
• Carsten Ihlemann and Viorica Sofronie-Stokkermans, "On Hierarchical Reasoning in Combinations of Theories", in AVACS Technical Report, (2010), Vol. 60, pp. 26 p.
Citation
Carsten Ihlemann and Viorica Sofronie-Stokkermans, "On Hierarchical Reasoning in Combinations of Theories", in AVACS Technical Report, (2010), Vol. 60, pp. 26 p.
Abstract
In this paper we study theory combinations over non-disjoint signatures in which hierarchical and modular reasoning is possible. We use a notion of locality of a theory extension parameterized by a closure operator on ground terms. We give criteria for recognizing these types of theory extensions. We then show that combinations of extensions of theories which are local in this extended sense have also a locality property and hence allow modular and hierarchical reasoning. We thus obtain parameterized decidability and complexity results for many (combinations of) theories important in verification.
Export
• Carsten Ihlemann and Viorica Sofronie-Stokkermans, "System Description: H-PILoT (Version 1.9)", in AVACS Technical Report, (2010), Vol. 61, pp. 45 p.
Citation
Carsten Ihlemann and Viorica Sofronie-Stokkermans, "System Description: H-PILoT (Version 1.9)", in AVACS Technical Report, (2010), Vol. 61, pp. 45 p.
Abstract
This system description provides an overview of H-PILoT (Hierarchical Proving by Instantiation in Local Theory extensions), a program for hierarchical reasoning in extensions of logical theories. H-PILoT reduces deduction problems in the theory extension to deduction problems in the base theory. Specialized provers and standard SMT solvers can be used for testing the satisfiability of the formulae obtained after the reduction. For a certain type of theory extension (namely for {\em local theory extensions}) this hierarchical reduction is sound and complete and -- if the formulae obtained this way belong to a fragment decidable in the base theory -- H-PILoT provides a decision procedure for testing satisfiability of ground formulae, and can also be used for model generation.
Export
• Swen Jacobs, Hierarchic Decision Procedures for Verification, PhD Thesis, Universität des Saarlandes, 2010.
Citation
Swen Jacobs, Hierarchic Decision Procedures for Verification, PhD Thesis, Universität des Saarlandes, 2010.
Export
• Tianxiang Lu, Stephan Merz, and Christoph Weidenbach, "Model Checking the Pastry Routing Protocol", in Proceedings of the 10th International Workshop Automatic Verification of Critical Systems, edited by Jens Bendisposto, Michael Leuschel, and Markus Roggenbach (Universität Düsseldorf, Düsseldorf, 2010), pp. 19-21.
Citation
Tianxiang Lu, Stephan Merz, and Christoph Weidenbach, "Model Checking the Pastry Routing Protocol", in Proceedings of the 10th International Workshop Automatic Verification of Critical Systems, edited by Jens Bendisposto, Michael Leuschel, and Markus Roggenbach (Universität Düsseldorf, Düsseldorf, 2010), pp. 19-21.
Abstract
Pastry is an algorithm for implementing a scalable distributed hash table over an underlying P2P network, an active area of research in distributed systems. Several implementations of Pastry are available and have been applied in practice, but no attempt has so far been made to formally describe the algorithm or to verify its properties. Since Pastry combines rather complex data structures, asynchronous communication, concurrency, resilience to \emph{churn} and fault tolerance, it makes an interesting target for verification. We have modeled Pastry's core routing algorithms in the specification language \texorpdfstring{\textrm{\upshape TLA\textsuperscript{+}}}{TLA+} and used its model checker \textsc{tlc} to analyze qualitative properties of Pastry such as \emph{correctness} and \emph{consistency}.
Export
• Andrey Rybalchenko and Viorica Sofronie-Stokkermans, "Constraint Solving for Interpolation," Journal of Symbolic Computation 45 (11), 1212-1233 (2010).
Citation
Andrey Rybalchenko and Viorica Sofronie-Stokkermans, "Constraint Solving for Interpolation," Journal of Symbolic Computation 45 (11), 1212-1233 (2010).
Abstract
Interpolation is an important component of recent methods for program verification. It provides a natural and effective means for computing the separation between the sets of ‘good’ and ‘bad’ states. The existing algorithms for interpolant generation are proof-based: They require explicit construction of proofs, from which interpolants can be computed. Construction of such proofs is a difficult task. We propose an algorithm for the generation of interpolants for the combined theory of linear arithmetic and uninterpreted function symbols that does not require a priori constructed proofs to derive interpolants. It uses a reduction of the problem to constraint solving in linear arithmetic, which allows application of existing highly optimized Linear Programming solvers in a black-box fashion. We provide experimental evidence of the practical applicability of our algorithm.
Export
• Viorica Sofronie-Stokkermans, "Hierarchical Reasoning for the Verification of Parametric Systems", in Automated Reasoning, edited by Jürgen Giesl and Reiner Hähnle (Springer, Berlin, 2010), pp. 171-187.
Citation
Viorica Sofronie-Stokkermans, "Hierarchical Reasoning for the Verification of Parametric Systems", in Automated Reasoning, edited by Jürgen Giesl and Reiner Hähnle (Springer, Berlin, 2010), pp. 171-187.
Abstract
We study certain classes of verification problems for parametric reactive and hybrid systems, and identify the types of logical theories which can be used for modeling such systems and the reasoning tasks which need to be solved in this context. We identify properties of the underlying theories which ensure that these classes of verification problems can be solved efficiently, give examples of theories with the desired properties, and illustrate the methods we use on several examples.
Export
• Martin Suda, Christoph Weidenbach, and Patrick Wischnewski, "On the saturation of YAGO", in Research Report, (2010), pp. 50 p.
Citation
Martin Suda, Christoph Weidenbach, and Patrick Wischnewski, "On the saturation of YAGO", in Research Report, (2010), pp. 50 p.
Export
• Martin Suda, Christoph Weidenbach, and Patrick Wischnewski, "On the Saturation of YAGO", in Automated Reasoning, edited by Jürgen Giesl and Reiner Hähnle (Springer, Berlin, 2010), pp. 441-456.
Citation
Martin Suda, Christoph Weidenbach, and Patrick Wischnewski, "On the Saturation of YAGO", in Automated Reasoning, edited by Jürgen Giesl and Reiner Hähnle (Springer, Berlin, 2010), pp. 441-456.
Abstract
YAGO is an automatically generated ontology out of Wikipedia and WordNet. It is eventually represented in a proprietary flat text file format and a core comprises 10 million facts and formulas. We present a translation of YAGO into the Bernays-Sch¨onfinkel Horn class with equality. A new variant of the superposition calculus is sound, complete and terminating for this class. Together with extended term indexing data structures the new calculus is implemented in Spass-YAGO. YAGO can be finitely saturated by Spass-YAGO in about 1 hour.We have found 49 inconsistencies in the original generated ontology which we have fixed. Spass-YAGO can then prove non-trivial conjectures with respect to the resulting saturated and consistent clause set of about 1.4 GB in less than one second.
Export
• Geoff Sutcliffe, Martin Suda, Alexandra Teyssandier, Nelson Dellis, and Gerard de Melo, "Progress Towards Effective Automated Reasoning with World Knowledge", in Proceedings of the Twenty-Third International Florida Artificial Intelligence Research Society Conference, edited by Hans W. Guesgen and R. Charles Murray (AAAI Press, Menlo Park, CA, 2010), pp. 110-115.
Citation
Geoff Sutcliffe, Martin Suda, Alexandra Teyssandier, Nelson Dellis, and Gerard de Melo, "Progress Towards Effective Automated Reasoning with World Knowledge", in Proceedings of the Twenty-Third International Florida Artificial Intelligence Research Society Conference, edited by Hans W. Guesgen and R. Charles Murray (AAAI Press, Menlo Park, CA, 2010), pp. 110-115.
Export
• Duc-Khanh Tran, Christopher Ringeissen, Silvio Ranise, and Helene Kirchner, "Combinations of Convex Theories: Modularity, Deduction Completeness and Explanation," Journal of Symbolic Computation 45 (2), 261-268 (2010).
Citation
Duc-Khanh Tran, Christopher Ringeissen, Silvio Ranise, and Helene Kirchner, "Combinations of Convex Theories: Modularity, Deduction Completeness and Explanation," Journal of Symbolic Computation 45 (2), 261-268 (2010).
Abstract
Decision procedures are key components of theorem provers and constraint satisfaction systems. Their modular combination is of prime interest for building efficient systems, but their effective use is often limited by poor interface capabilities, when such procedures only provide a simple sat/unsat'' answer. In this paper, we develop a framework to design cooperation schemas between such procedures while maintaining modularity of their interfaces. First, we use the framework to specify and prove the correctness of classic combination schemas by Nelson-Oppen and Shostak. Second, we introduce the concept of deduction complete satisfiability procedures, we show how to build them for large classes of theories, then we provide a schema to modularly combine them. Third, we consider the problem of modularly constructing explanations for combinations by re-using available proof-producing procedures for the component theories.
Export
• Christoph Weidenbach and Patrick Wischnewski, "Subterm Contextual Rewriting," AI Communications 23 (2-3), 97-109 (2010).
Citation
Christoph Weidenbach and Patrick Wischnewski, "Subterm Contextual Rewriting," AI Communications 23 (2-3), 97-109 (2010).
Export
• Ernst Althaus, Evgeny Kruglov, and Christoph Weidenbach, "Superposition Modulo Linear Arithmetic SUP(LA)", in Frontiers of Combining Systems, edited by Silvio Ghilardi and Roberto Sebastiani (Springer, Berlin, 2009), pp. 84-99.
Citation
Ernst Althaus, Evgeny Kruglov, and Christoph Weidenbach, "Superposition Modulo Linear Arithmetic SUP(LA)", in Frontiers of Combining Systems, edited by Silvio Ghilardi and Roberto Sebastiani (Springer, Berlin, 2009), pp. 84-99.
Export
• Peter Baumgartner and Uwe Waldmann, "Superposition and Model Evolution Combined", in Automated Deduction, CADE-22, 22nd International Conference on Automated Deduction, edited by Renate A. Schmidt (Springer, Berlin, Germany, 2009), pp. 17-34.
Citation
Peter Baumgartner and Uwe Waldmann, "Superposition and Model Evolution Combined", in Automated Deduction, CADE-22, 22nd International Conference on Automated Deduction, edited by Renate A. Schmidt (Springer, Berlin, Germany, 2009), pp. 17-34.
Abstract
We present a new calculus for first-order theorem proving with equality, ME+Sup, which generalizes both the Superposition calculus and the Model Evolution calculus (with equality) by integrating their inference rules and redundancy criteria in a non-trivial way. The main motivation is to combine the advantageous features of both---rather complementary---calculi in a single framework. For instance, Model Evolution, as a lifted version of the propositional DPLL procedure, contributes a non-ground splitting rule that effectively permits to split a clause into non variable disjoint subclauses. In the paper we present the calculus in detail. Our main result is its completeness under semantically justified redundancy criteria and simplification rules.
Export
• Dilyana Dimova, On the Translation of Timed Automata into First-order Logic, Master Thesis, Universität des Saarlandes, 2009.
Citation
Dilyana Dimova, On the Translation of Timed Automata into First-order Logic, Master Thesis, Universität des Saarlandes, 2009.
Export
• Christian Dreßler, Automatic Analysis of Tree-Based Feature Models with SPASS, Master Thesis, Universität des Saarlandes, 2009.
Citation
Christian Dreßler, Automatic Analysis of Tree-Based Feature Models with SPASS, Master Thesis, Universität des Saarlandes, 2009.
Export
• Arnaud Fietzke and Christoph Weidenbach, "Labelled Splitting," Annals of Mathematics and Artificial Intelligence 55 (1-2), 3-33 (2009).
Citation
Arnaud Fietzke and Christoph Weidenbach, "Labelled Splitting," Annals of Mathematics and Artificial Intelligence 55 (1-2), 3-33 (2009).
Export
• Matthias Horbach and Christoph Weidenbach, "Decidability Results for Saturation-based Model Building", in Research Report, (2009), pp. 38 p.
Citation
Matthias Horbach and Christoph Weidenbach, "Decidability Results for Saturation-based Model Building", in Research Report, (2009), pp. 38 p.
Abstract
Saturation-based calculi such as superposition can be successfully instantiated to decision procedures for many decidable fragments of first-order logic. In case of termination without generating an empty clause, a saturated clause set implicitly represents a minimal model for all clauses, based on the underlying term ordering of the superposition calculus. In general, it is not decidable whether a ground atom, a clause or even a formula holds in this minimal model of a satisfiable saturated clause set. Based on an extension of our superposition calculus for fixed domains with syntactic disequality constraints in a non-equational setting, we describe models given by ARM (Atomic Representations of term Models) or DIG (Disjunctions of Implicit Generalizations) representations as minimal models of finite saturated clause sets. This allows us to present several new decidability results for validity in such models. These results extend in particular the known decidability results for ARM and DIG representations.
Export
• Matthias Horbach and Christoph Weidenbach, "Decidability Results for Saturation-Based Model Building", in 22nd International Conference on Automated Deduction (CADE-22), edited by Renate Schmidt (Springer, Heidelberg, 2009), pp. 404-420.
Citation
Matthias Horbach and Christoph Weidenbach, "Decidability Results for Saturation-Based Model Building", in 22nd International Conference on Automated Deduction (CADE-22), edited by Renate Schmidt (Springer, Heidelberg, 2009), pp. 404-420.
Abstract
Saturation-based calculi such as superposition can be successfully instantiated to decision procedures for many decidable fragments of first-order logic. In case of termination without generating an empty clause, a saturated clause set implicitly represents a minimal model for all clauses, based on the underlying term ordering of the superposition calculus. In general, it is not decidable whether a ground atom, a clause or even a formula holds in this minimal model of a satisfiable saturated clause set. We extend our superposition calculus for fixed domains with syntactic disequality constraints in a non-equational setting. Based on this calculus, we present several new decidability results for validity in the minimal model of a satisfiable finitely saturated clause set that in particular extend the decidability results known for ARM (Atomic Representations of term Models) and DIG (Disjunctions of Implicit Generalizations) model representations.
Export
• Matthias Horbach and Christoph Weidenbach, "Deciding the Inductive Validity of FOR ALL THERE EXISTS * Queries", in CSL, (Springer, Heidelberg, 2009), pp. 332-347.
Citation
Matthias Horbach and Christoph Weidenbach, "Deciding the Inductive Validity of FOR ALL THERE EXISTS * Queries", in CSL, (Springer, Heidelberg, 2009), pp. 332-347.
Export
• Matthias Horbach and Christoph Weidenbach, "Superposition for Fixed Domains", in Research Report, (2009), pp. 49 p.
Citation
Matthias Horbach and Christoph Weidenbach, "Superposition for Fixed Domains", in Research Report, (2009), pp. 49 p.
Abstract
Superposition is an established decision procedure for a variety of first-order logic theories represented by sets of clauses. A satisfiable theory, saturated by superposition, implicitly defines a minimal term-generated model for the theory. Proving universal properties with respect to a saturated theory directly leads to a modification of the minimal model's term-generated domain, as new Skolem functions are introduced. For many applications, this is not desired. Therefore, we propose the first superposition calculus that can explicitly represent existentially quantified variables and can thus compute with respect to a given domain. This calculus is sound and refutationally complete in the limit for a first-order fixed domain semantics. For saturated Horn theories and classes of positive formulas, we can even employ the calculus to prove properties of the minimal model itself, going beyond the scope of known superposition-based approaches.
Export
• Matthias Horbach and Christoph Weidenbach, "Deciding the Inductive Validity of Forall Exists* Queries", (2009).
Citation
Matthias Horbach and Christoph Weidenbach, "Deciding the Inductive Validity of Forall Exists* Queries", (2009).
Abstract
We present a new saturation-based decidability result for inductive validity. Let $\Sigma$ be a finite signature in which all function symbols are at most unary and let $N$ be a satisfiable Horn clause set without equality in which all positive literals are linear. If $N\cup\{A_1,\ldots,A_n\rightarrow\}$ belongs to a finitely saturating clause class, then it is decidable whether a sentence of the form $\forall\exists^* (A_1\wedge\ldots\wedge A_n)$ is valid in the minimal model of $N$.
Export
• Carsten Ihlemann and Viorica Sofronie-Stokkermans, "System Description: H-PILoT", in Automated Deduction - CADE-22, edited by Renate Schmidt (Springer, Berlin, 2009), pp. 131-139.
Citation
Carsten Ihlemann and Viorica Sofronie-Stokkermans, "System Description: H-PILoT", in Automated Deduction - CADE-22, edited by Renate Schmidt (Springer, Berlin, 2009), pp. 131-139.
Abstract
H-PILoT (Hierarchical Proving by Instantiation in Local Theory extensions) is a program for hierarchical reasoning in extensions of logical theories with additional functions axiomatized by a set of (universally quantified) clauses: deduction problems in the theory extension are reduced to deduction problems in the base theory. Specialized provers, as well as standard SMT solvers, are then used for testing the satisfiability of the formulae obtained after the reduction. The hierarchical reduction used in H-PILoT is always sound; it is complete for the class of so-called local extensions of a base theory. If the clauses obtained by this reduction belong to a fragment decidable in the base theory, H-PILoT provides a decision procedure for testing satisfiability of ground formulae w.r.t.\ a theory extension, and can also be used for model generation. This is the major advantage of H-PILoT compared with other state-of-the art SMT solvers. H-PILoT can alternatively be used as a tool for steering'' the instantiation mechanism of standard SMT provers, in order to provide decision procedures in the case of local theory extensions. This system description provides an overview of H-PILoT and illustrates on some examples the main advantage of using H-PILoT for satisfiability checking in local extensions, in comparison with the performance of general state of the art SMT-provers.
Export
• Swen Jacobs, "Incremental Instance Generation in Local Reasoning", in Computer Aided Verification, edited by Ahmed Bouajjani and Oded Maler (Springer, Berlin, 2009), pp. 368-382.
Citation
Swen Jacobs, "Incremental Instance Generation in Local Reasoning", in Computer Aided Verification, edited by Ahmed Bouajjani and Oded Maler (Springer, Berlin, 2009), pp. 368-382.
Abstract
Many verification approaches use SMT solvers in some form, and are limited by their incomplete handling of quantified formulas. Local reasoning allows to handle SMT problems involving a certain class of universally quantified formulas in a complete way by instantiation to a finite set of ground formulas. We present a method to generate these instances incrementally, in order to provide a more efficient way of solving these satisfiability problems. The incremental instantiation is guided semantically, inspired by the instance generation approach to first-order theorem proving. Our method is sound and complete, and terminates on both satisfiable and unsatisfiable input after generating a subset of the instances needed in standard local reasoning. Experimental results show that for a large class of examples the incremental approach is substantially more efficient than eager generation of all instances.
Export
• Manuel Lamotte-Schubert and Christoph Weidenbach, "Analysis of Authorizations in SAP R/3", in Proceedings of the 7th International Workshop on First-Order Theorem Proving (FTP'09), (2009), pp. 90-104.
Citation
Manuel Lamotte-Schubert and Christoph Weidenbach, "Analysis of Authorizations in SAP R/3", in Proceedings of the 7th International Workshop on First-Order Theorem Proving (FTP'09), (2009), pp. 90-104.
Abstract
Today many companies use an ERP (Enterprise Resource Planning) system such as SAP R/3 to run their daily business ranging from financial issues down to the actual control of a production line. Already due to their sheer size, these systems are very complex. In particular, developing and maintaining the authorization setup is a challenge. The goal of our effort is to automatically analyze the authorization setup of an SAP R/3 system against business policies. To this end we formalize the processes, authorization setup as well as the business policies in first-order logic. Then, properties can be (dis)proven fully automatically with our theorem prover Spass. We exemplify our approach on the purchase process, a typical constituent of any SAP R/3 installation.
Export
• Manuel Lamotte-Schubert and Christoph Weidenbach, "Analysis of Authorizations in SAP R/3", in FTP 2009 Workshop Proceedings, (2009), pp. 90-104.
Citation
Manuel Lamotte-Schubert and Christoph Weidenbach, "Analysis of Authorizations in SAP R/3", in FTP 2009 Workshop Proceedings, (2009), pp. 90-104.
Abstract
Today many companies use an ERP (Enterprise Resource Planning) system such as SAP R/3~to run their daily business ranging from financial issues down to the actual control of a production line. Already due to their sheer size, these systems are very complex. In particular, developing and maintaining the authorization setup is a challenge. The goal of our effort is to automatically analyze the authorization setup of an SAP R/3~system against business policies. To this end we formalize the processes, authorization setup as well as the business policies in first-order logic. Then, properties can be (dis)proven fully automatically with our theorem prover \textsc{Spass}. We exemplify our approach on the purchase process, a typical constituent of any SAP R/3~installation.
Export
• Christopher Lynch, Narendran Paliath, Franz Baader, Silvio Ghilardi, Miki Hermann, Viorica Sofronie-Stokkermans, and Ashish Tiwari (eds), Joint proceedings of UNIF 2009 (23nd International Workshop on Unification) and ADDCT 2009 (Automated Deduction: Decidability, Complexity, Tractability). (-, -, 2009).
Citation
Christopher Lynch, Narendran Paliath, Franz Baader, Silvio Ghilardi, Miki Hermann, Viorica Sofronie-Stokkermans, and Ashish Tiwari (eds), Joint proceedings of UNIF 2009 (23nd International Workshop on Unification) and ADDCT 2009 (Automated Deduction: Decidability, Complexity, Tractability). (-, -, 2009).
Export
• Nicolas Peltier and Viorica Sofronie-Stokkermans (eds), First-Order Theorem Proving: FTP 2009 Workshop Proceedings. (University of Oslo, Department of Informatics, Oslo, Norway, 2009).
Citation
Nicolas Peltier and Viorica Sofronie-Stokkermans (eds), First-Order Theorem Proving: FTP 2009 Workshop Proceedings. (University of Oslo, Department of Informatics, Oslo, Norway, 2009).
Export
• Andrey Rybalchenko and Viorica Sofronie-Stokkermans, "Constraint Solving for Interpolation", (2009).
Citation
Andrey Rybalchenko and Viorica Sofronie-Stokkermans, "Constraint Solving for Interpolation", (2009).
Export
• Viorica Sofronie-Stokkermans, "Locality results for certain extensions of theories with bridging functions", in Automated Deduction - CADE-22, edited by Renate A. Schmidt (Springer, Berlin, 2009).
Citation
Viorica Sofronie-Stokkermans, "Locality results for certain extensions of theories with bridging functions", in Automated Deduction - CADE-22, edited by Renate A. Schmidt (Springer, Berlin, 2009).
Abstract
n this paper we study possibilities of reasoning about functions over theories of data types which satisfy certain recursion (or homomorphism) properties, with a focus on emphasizing possibilities of hierarchical and modular reasoning in such extensions and combinations thereof. We start by considering theories of absolutely free data structures, and continue by studying extensions of such theories with selectors, with functions which attach scalar data to the data structures and with additional functions defined using a certain type of recursion axioms (possibly having values in a different -- e.g.\ numeric -- domain). We show that in these cases locality results can be established. This allows us to reduce the task of reasoning about the class of recursive functions we consider to reasoning in the underlying theory of absolutely free data structures (resp. in a combination of the theory of absolutely free data structures with the theory attached with the domains of the additional functions). We then show that similar results can be obtained if we relax some assumptions about the absolute freeness of the underlying theory of data types. We investigate the applications of these ideas in verification and cryptography.
Export
• Viorica Sofronie-Stokkermans, "Reasoning in Complex Theories and Applications. Advanced Lecture, ESSLLI 2009", (ESSLLI 2009 CDrom, 2009).
Citation
Viorica Sofronie-Stokkermans, "Reasoning in Complex Theories and Applications. Advanced Lecture, ESSLLI 2009", (ESSLLI 2009 CDrom, 2009).
Export
• Viorica Sofronie-Stokkermans, "Sheaves and geometric logic and applications to modular verification of complex systems," Electronic Notes in Theoretical Computer Science 230, 161-187 (2009).
Citation
Viorica Sofronie-Stokkermans, "Sheaves and geometric logic and applications to modular verification of complex systems," Electronic Notes in Theoretical Computer Science 230, 161-187 (2009).
Abstract
In this paper we show that states, transitions and behavior of concurrent systems can often be modeled as sheaves over a suitable topological space. In this context, geometric logic can be used to describe which local properties, of individual systems, are preserved, at a global level, when interconnecting the systems. The main area of application is to modular verification of complex systems. We illustrate our ideas by means of an example involving a family of interacting controllers for trains on a rail track.
Export
• Martin Suda, Patrick Wischnewski, Manuel Lamotte-Schubert, and Gerard de Melo, "External Sources of Axioms in Automated Theorem Proving", in KI 2009: Advances in Artificial Intelligence, (Springer, Berlin, 2009), pp. 281-288.
Citation
Martin Suda, Patrick Wischnewski, Manuel Lamotte-Schubert, and Gerard de Melo, "External Sources of Axioms in Automated Theorem Proving", in KI 2009: Advances in Artificial Intelligence, (Springer, Berlin, 2009), pp. 281-288.
Abstract
In recent years there has been a growing demand for Automated Theorem Proving (ATP) in large theories, which often have more axioms than can be handled effectively as normal internal axioms. This work addresses the issues of accessing \emph{external sources of axioms} from a first-order logic ATP system, and presents an implemented ATP system that retrieves external axioms asynchronously, on demand.
Export
• Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Martin Suda, and Patrick Wischnewski, "SPASS Version 3.5", in 22nd International Conference on Automated Deduction (CADE-22), edited by Renate A. Schmidt (Springer, Heidelberg, Germany, 2009), pp. 140-145.
Citation
Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Martin Suda, and Patrick Wischnewski, "SPASS Version 3.5", in 22nd International Conference on Automated Deduction (CADE-22), edited by Renate A. Schmidt (Springer, Heidelberg, Germany, 2009), pp. 140-145.
Export
• Christoph Weidenbach and Patrick Wischnewski, "Contextual Rewriting", (2009).
Citation
Christoph Weidenbach and Patrick Wischnewski, "Contextual Rewriting", (2009).
Export
• Franz Baader, Silvio Ghilardi, Miki Hermann, Ulrike Sattler, and Viorica Sofronie-Stokkermans (eds), Workshop: Complexity, Expressibility, and Decidability in Automated Reasoning - CEDAR'08. (CEDAR, Sydney, 2008).
Citation
Franz Baader, Silvio Ghilardi, Miki Hermann, Ulrike Sattler, and Viorica Sofronie-Stokkermans (eds), Workshop: Complexity, Expressibility, and Decidability in Automated Reasoning - CEDAR'08. (CEDAR, Sydney, 2008).
Export
• Arnaud Luc Fietzke and Christoph Weidenbach, "Labelled splitting", in Research Report, (2008), pp. 45 p.
Citation
Arnaud Luc Fietzke and Christoph Weidenbach, "Labelled splitting", in Research Report, (2008), pp. 45 p.
Abstract
We define a superposition calculus with explicit splitting and an explicit, new backtracking rule on the basis of labelled clauses. For the first time we show a superposition calculus with explicit backtracking rule sound and complete. The new backtracking rule advances backtracking with branch condensing known from SPASS. An experimental evaluation of an implementation of the new rule shows that it improves considerably the previous SPASS splitting implementation. Finally, we discuss the relationship between labelled first-order splitting and DPLL style splitting with intelligent backtracking and clause learning.
Export
• Arnaud Luc Fietzke and Christoph Weidenbach, "Labelled Splitting", in Automated Reasoning, edited by Allesandro Armando, Peter Baumgartner, and Gilles Dowek (Springer, Berlin, 2008), pp. 459-474.
Citation
Arnaud Luc Fietzke and Christoph Weidenbach, "Labelled Splitting", in Automated Reasoning, edited by Allesandro Armando, Peter Baumgartner, and Gilles Dowek (Springer, Berlin, 2008), pp. 459-474.
Export
• Thomas Hillenbrand, Superposition and Decision Procedures - Back and Forth, PhD Thesis, Universität des Saarlandes, 2009.
Citation
Thomas Hillenbrand, Superposition and Decision Procedures - Back and Forth, PhD Thesis, Universität des Saarlandes, 2009.
Abstract
Two apparently different approaches to automating deduction are mentioned in the title; they are the subject of a debate on big engines vs.\ little engines of proof''. The contributions in this thesis advocate that these two strands of research can interplay in subtle and sometimes unexpected ways, such that mutual pervasion can lead to intriguing results: Firstly, superposition can be run on top of decision procedures. This we demonstrate for the class of Shostak theories, incorporating a little engine into a big one. As another instance of decision procedures within superposition, we show that ground confluent rewrite systems, which decide entailment problems in equational logic, can be harnessed for detecting redundancies in superposition derivations. Secondly, superposition can be employed as proof-theoretic means underneath combined decision procedures: We re-establish the correctness of the Nelson-Oppen procedure as an instance of the completeness of superposition. Thirdly, superposition can be used as a decision procedure for many interesting theories, turning a big engine into a little one. For the theory of bits and of fixed-size bitvectors, we suggest a rephrased axiomatization combined with a transformation of conjectures, based on which superposition decides the universal fragment. Furthermore, with a modification of lifting, we adapt superposition to the theory of bounded domains and give a decision procedure, which captures the Bernays-Schönfinkel class as well.
Export
• Matthias Horbach and Christoph Weidenbach, "Superposition for Fixed Domains", in Computer Science Logic: 22nd International Workshop, CSL 2008, 17th Annual Conference of the EACSL, edited by Michael Kaminski and Simone Martini (Springer, Berlin, 2008), pp. 293-307.
Citation
Matthias Horbach and Christoph Weidenbach, "Superposition for Fixed Domains", in Computer Science Logic: 22nd International Workshop, CSL 2008, 17th Annual Conference of the EACSL, edited by Michael Kaminski and Simone Martini (Springer, Berlin, 2008), pp. 293-307.
Export
• Carsten Ihlemann, Swen Jacobs, and Viorica Sofronie-Stokkermans, "On local reasoning in verification", in Tools and Algorithms for the Construction and Analysis of Systems: 14th International Conference, TACAS 2008 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, edited by C. R. Ramakrishnan and Jakob Rehof (Springer, New York, 2008), pp. 265-281.
Citation
Carsten Ihlemann, Swen Jacobs, and Viorica Sofronie-Stokkermans, "On local reasoning in verification", in Tools and Algorithms for the Construction and Analysis of Systems: 14th International Conference, TACAS 2008 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, edited by C. R. Ramakrishnan and Jakob Rehof (Springer, New York, 2008), pp. 265-281.
Abstract
We present a general framework which allows to identify complex theories important in verification for which efficient reasoning methods exist. The framework we present is based on a general notion of locality. We show that locality considerations allow us to obtain parameterized decidability and complexity results for many (combinations of) theories important in verification in general and in the verification of parametric systems in particular. We give numerous examples; in particular we show that several theories of data structures studied in the verification literature are local extensions of a base theory. The general framework we use allows us to identify situations in which some of the syntactical restrictions imposed in previous papers can be relaxed.
Export
• Swen Jacobs, "Incremental Instance Generation in Local Reasoning", in Workshop: Complexity, Expressibility, and Decidability in Automated Reasoning – CEDAR’08, edited by Franz Baader, Silvio Ghilardi, Miki Hermann, Ulrike Sattler, and Viorica Sofronie-Stokkermans (CEDAR, Sydney, Australia, 2008), pp. 47-62.
Citation
Swen Jacobs, "Incremental Instance Generation in Local Reasoning", in Workshop: Complexity, Expressibility, and Decidability in Automated Reasoning – CEDAR’08, edited by Franz Baader, Silvio Ghilardi, Miki Hermann, Ulrike Sattler, and Viorica Sofronie-Stokkermans (CEDAR, Sydney, Australia, 2008), pp. 47-62.
Abstract
Local reasoning allows to handle SMT problems involving a certain class of universally quantified formulas in a complete way by instantiation to a finite set of ground formulas. We present a method to generate this set incrementally, in order to provide a more efficient way of solving these satisfiability problems. The incremental instantiation is guided semantically, inspired by the instance generation approach to first-order theorem proving. Our method is sound and complete, and terminates on both satisfiable and unsatisfiable input after generating a subset of the instances needed in standard local reasoning.
Export
• Evgeny Kruglov, Superposition Modulo Linear Arithmetic, Master Thesis, Universität des Saarlandes, 2008.
Citation
Evgeny Kruglov, Superposition Modulo Linear Arithmetic, Master Thesis, Universität des Saarlandes, 2008.
Export
• Manuel Lamotte, Analysis of Authorizations in SAP R/3, Master Thesis, Universität des Saarlandes, 2008.
Citation
Manuel Lamotte, Analysis of Authorizations in SAP R/3, Master Thesis, Universität des Saarlandes, 2008.
Abstract
Today many companies use an ERP (Enterprise Resource Planning) system such as the SAP R/3 system to run their daily business ranging from financial issues down to the actual control of a production line. These systems are very complex from the view of administration and authorization. Hence they include a high potential for errors. In this thesis I analyze the authorization concept of the SAP R/3 system as well as different business regulations and construct a corresponding model in first-order logic. This model can be used to check the existence of errors automatically, i.e. a contradiction between given authorizations and a valid business regulation. The tool I use for these checks is the theorem prover \textscSpass which has been developed at the Max Planck Institute for Informatics. I selected the purchase process as an example to explore the model construction because it is a typical constituent of the SAP R/3 system.
Export
• Christopher Lynch and Duc-Khanh Tran, "SMELS: Satisfiability Modulo Equality with Lazy Superposition", in Automated Technology for Verification and Analysis, edited by Sungdeok Cha, Jin-Young Choi, Moonzoo Kim, Insup Lee, and Mahesh Viswanathan (Springer, Berlin, 2008), pp. 186-200.
Citation
Christopher Lynch and Duc-Khanh Tran, "SMELS: Satisfiability Modulo Equality with Lazy Superposition", in Automated Technology for Verification and Analysis, edited by Sungdeok Cha, Jin-Young Choi, Moonzoo Kim, Insup Lee, and Mahesh Viswanathan (Springer, Berlin, 2008), pp. 186-200.
Export
• Rostislav Rusev, Bitvector Reasoning with SPASS, Master Thesis, Universität des Saarlandes, 2008.
Citation
Rostislav Rusev, Bitvector Reasoning with SPASS, Master Thesis, Universität des Saarlandes, 2008.
Export
• Viorica Sofronie-Stokkermans, "Reasoning in Complex Theories and Applications", in KI 2008: Tutorial 2, (KI, Kaiserslautern, 2008), pp. 1-64.
Citation
Viorica Sofronie-Stokkermans, "Reasoning in Complex Theories and Applications", in KI 2008: Tutorial 2, (KI, Kaiserslautern, 2008), pp. 1-64.
Abstract
One of the most important objectives of the research in mathematics and computer science is to obtain means of reasoning in and about complex systems. These can be, for instance complex mathematical theories; programs, or generally reactive or hybrid systems; distributed databases; or complex systems in general (e.g. multi-agent systems or reactive or hybrid systems with embedded software, whose behavior is controlled by databases, reasoning about knowledge and belief, planning mechanisms, or programs). Proving that such systems have certain properties (e.g. that they are safe, that they behave correctly, or that the information they use does not contain inconsistencies) is extremely important: In safety-critical systems (such as cars, trains, planes, or power-plants) even small mistakes can provoke disasters. Since the amount of data which has to be handled in verification tasks is usually huge, computer support is indispensable. The dream of the scientists is to provide such correctness proofs automatically. This goal cannot be reached in its full generality: As shown by undecidability results going back to the work of Gödel, Church and Turing, it is impossible to write a program for checking arbitrary properties of general systems. However, for concrete application domains, automatic procedures exist. It is therefore very important to identify situations in which automated verification of complex systems is possible. For this, it is essential to identify theories which are decidable, preferably with low complexity, and - since concrete problems often are quite heterogeneous in nature - to obtain methods for efficiently combining decision procedures. The goal of the tutorial is to give a comprehensive, in-depth perspective of recent advances in the field of reasoning in complex logical theories, and to present applications of these results in various areas ranging from formal verification to reasoning about knowledge. The tutorial introduces the general principles underlying reasoning in complex theories from a unifying perspective, gives a survey of recent achievements in the field, and illustrates the problems and their solutions using a selection of examples from mathematics, verification, and knowledge representation.
Export
• Viorica Sofronie-Stokkermans, "Interpolation in local theory extensions," Logical Methods in Computer Science 4 (4), Art.1.1-31 (2008).
Citation
Viorica Sofronie-Stokkermans, "Interpolation in local theory extensions," Logical Methods in Computer Science 4 (4), Art.1.1-31 (2008).
Abstract
In this paper we study interpolation in local extensions of a base theory. We identify situations in which it is possible to obtain interpolants in a hierarchical manner, by using a prover and a procedure for generating interpolants in the base theory as black-boxes. We present several examples of theory extensions in which interpolants can be computed this way, and discuss applications in verification, knowledge representation, and modular reasoning in combinations of local theories.
Export
• Viorica Sofronie-Stokkermans, "Locality and subsumption testing in EL and some of its extensions", in Advances in Modal Logic 7: [Proceedings of the AiML 2008], edited by Carlos Areces and Robert Goldblatt (College Publications, London, 2008), pp. 315-339.
Citation
Viorica Sofronie-Stokkermans, "Locality and subsumption testing in EL and some of its extensions", in Advances in Modal Logic 7: [Proceedings of the AiML 2008], edited by Carlos Areces and Robert Goldblatt (College Publications, London, 2008), pp. 315-339.
Abstract
In this paper we show that subsumption problems in many lightweight description logics (including ${\cal EL}$) can be expressed as uniform word problems in classes of semilattices with monotone operators. We use possibilities of efficient local reasoning in such classes of algebras to obtain uniform PTIME decision procedures for CBox subsumption in ${\cal EL}$ and extensions thereof. These locality considerations allow us to present a new family of logics which extend ${\cal EL}$ with $n$-ary roles and numerical domains and also a new extension of ${\cal EL}^+$.
Export
• Viorica Sofronie-Stokkermans, "Locality and subsumption testing in EL and some of its extensions", in Proceedings of the 21st International Workshop on Description Logics (DL-2008), edited by Franz Baader, Carsten Lutz, and Boris Motik (CEUR, Aachen, 2008), pp. Art.31.1-11.
Citation
Viorica Sofronie-Stokkermans, "Locality and subsumption testing in EL and some of its extensions", in Proceedings of the 21st International Workshop on Description Logics (DL-2008), edited by Franz Baader, Carsten Lutz, and Boris Motik (CEUR, Aachen, 2008), pp. Art.31.1-11.
Abstract
In this paper we show that subsumption problems in many lightweight description logics (including ${\cal EL}$) can be expressed as uniform word problems in classes of semilattices with monotone operators. We use possibilities of efficient local reasoning in such classes of algebras to obtain uniform PTIME decision procedures for CBox subsumption in ${\cal EL}$ and extensions thereof. These locality considerations allow us to present a new family of logics which extend ${\cal EL}$ and also a new extension of ${\cal EL}^+$.
Export
• Viorica Sofronie-Stokkermans, "Efficient hierarchical reasoning about functions over numerical domains", in KI 2008: Advances in Artificial Intelligence: 31st Annual German Conference on AI, KI 2008, edited by Andreas R. Dengel, Karsten Berns, Thomas M. Breuel, Frank Bomarius, and Thomas R. Roth-Berghofer (Springer, Berlin, 2008), pp. 135-143.
Citation
Viorica Sofronie-Stokkermans, "Efficient hierarchical reasoning about functions over numerical domains", in KI 2008: Advances in Artificial Intelligence: 31st Annual German Conference on AI, KI 2008, edited by Andreas R. Dengel, Karsten Berns, Thomas M. Breuel, Frank Bomarius, and Thomas R. Roth-Berghofer (Springer, Berlin, 2008), pp. 135-143.
Abstract
We show that many properties studied in mathematical analysis (e.g.\ monotonicity, boundedness, inverse or Lipschitz properties, possibly combined with continuity and/or derivability) are expressible as axioms in a class for which sound and complete hierarchical proof methods for testing satisfiability of ground formulae exist. The results are useful for automated reasoning in analysis, and in the verification of hybrid systems.
Export
• Viorica Sofronie-Stokkermans, "Sheaves and Geometric Logic and Applications to Modular Verification of Complex Systems", in AVACS Technical Report, (2008), Vol. 46.
Citation
Viorica Sofronie-Stokkermans, "Sheaves and Geometric Logic and Applications to Modular Verification of Complex Systems", in AVACS Technical Report, (2008), Vol. 46.
Abstract
In this paper we show that states, transitions and behavior of concurrent systems can often be modeled as sheaves over a suitable topological space (where the topology expresses how the interacting systems share the information). This allows us to use results from categorical logic (and in particular geometric logic) to describe which type of properties are transferred, if valid locally in all component systems, also at a global level, to the system obtained by interconnecting the individual systems. The main area of application is to modular verification of complex systems. We illustrate the ideas by means of an example involving a family of interacting controllers for trains on a rail track.
Export
• Viorica Sofronie-Stokkermans, "Efficient Hierarchical Reasoning about Functions over Numerical Domains", in AVACS Technical Report, (2008), Vol. 45, pp. 17 p.
Citation
Viorica Sofronie-Stokkermans, "Efficient Hierarchical Reasoning about Functions over Numerical Domains", in AVACS Technical Report, (2008), Vol. 45, pp. 17 p.
Abstract
We show that many properties studied in mathematical analysis (monotonicity, boundedness, inverse, Lipschitz properties, possibly combined with continuity or derivability) are expressible by formulae in a class for which sound and complete hierarchical proof methods for testing satisfiability of sets of ground clauses exist. The results are useful for automated reasoning in mathematical analysis and for the verification of hybrid systems.
Export
• Christoph Weidenbach and Patrick Wischnewski, "Contextual Rewriting in SPASS", in PAAR-2008/ESHOL-2008: First International Workshop on Practical Aspects of Automated Reasoning, edited by Boris Konev, Renate A. Schmidt, and Stephan Schulz (CEUR-WS.org, RHTW Aachen, 2008), pp. 115-124.
Citation
Christoph Weidenbach and Patrick Wischnewski, "Contextual Rewriting in SPASS", in PAAR-2008/ESHOL-2008: First International Workshop on Practical Aspects of Automated Reasoning, edited by Boris Konev, Renate A. Schmidt, and Stephan Schulz (CEUR-WS.org, RHTW Aachen, 2008), pp. 115-124.
Export
• Werner Damm, Stefan Disch, Hardi Hungar, Swen Jacobs, Jun Pang, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, and Boris Wirtz, "Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space", in Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007, edited by Kedar S. Namjoshi, Tomohiro Yoneda, Teruo Higashino, and Yoshio Okamura (Springer, Berlin, Germany, 2007), pp. 425-440.
Citation
Werner Damm, Stefan Disch, Hardi Hungar, Swen Jacobs, Jun Pang, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, and Boris Wirtz, "Exact State Set Representations in the Verification of Linear Hybrid Systems with Large Discrete State Space", in Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007, edited by Kedar S. Namjoshi, Tomohiro Yoneda, Teruo Higashino, and Yoshio Okamura (Springer, Berlin, Germany, 2007), pp. 425-440.
Abstract
We propose algorithms significantly extending the limits for maintaining exact representations in the verification of linear hybrid systems with large discrete state spaces. We use AND-Inverter Graphs (AIGs) extended with linear constraints (LinAIGs) as symbolic representation of the hybrid state space, and show how methods for maintaining compactness of AIGs can be lifted to support model-checking of linear hybrid systems with large discrete state spaces. This builds on a novel approach for eliminating sets of redundant constraints in such rich hybrid state representations by a suitable exploitation of the capabilities of SMT solvers, which is of independent value beyond the application context studied in this paper. We used a benchmark derived from an Airbus flap control system (containing $2^{20}$ discrete states) to demonstrate the relevance of the approach.
Export
• Christian Dreßler, First-order Proof Documentation, Bachelor Thesis, Universität des Saarlandes, 2007.
Citation
Christian Dreßler, First-order Proof Documentation, Bachelor Thesis, Universität des Saarlandes, 2007.
Export
• Johannes Faber, Swen Jacobs, and Viorica Sofronie-Stokkermans, "Verifying CSP-OZ-DC specifications with complex data types and timing parameters", in Integrated Formal Methods: 6th International Conference, IFM 2007, edited by Jim Davies and Jeremy Gibbons (Springer, Berlin, Germany, 2007), pp. 233-252.
Citation
Johannes Faber, Swen Jacobs, and Viorica Sofronie-Stokkermans, "Verifying CSP-OZ-DC specifications with complex data types and timing parameters", in Integrated Formal Methods: 6th International Conference, IFM 2007, edited by Jim Davies and Jeremy Gibbons (Springer, Berlin, Germany, 2007), pp. 233-252.
Export
• Arnaud Fietzke, Labelled Splitting, Master Thesis, Universität des Saarlandes, 2007.
Citation
Arnaud Fietzke, Labelled Splitting, Master Thesis, Universität des Saarlandes, 2007.
Abstract
Saturation-based theorem provers are typically based on a calculus consisting of inference and reduction rules that operate on sets of clauses. While inference rules produce new clauses, reduction rules allow the removal or simplification of redundant clauses and are an essential ingredient for efficient implementations. The power of reduction rules can be further amplified by the use of the splitting rule, which is based on explicit case analysis on variable- disjoint components of a clause. In this thesis, I give a formalization of splitting and backtracking for first-order logic using a labelling scheme that annotates clauses and clause sets with additional information, and I present soundness and completeness results for the corresponding calculus. The backtracking process as formalized here generalizes optimizations that are currently being used, and I present the results of integrating the improved backtracking into SPASS.
Export
• Jörn Freiheit and Fabrice Zangl, "Model-based User-interface Management for Public Services," Electronic Journal of e-Government 5 (1), 53-62 (2007).
Citation
Jörn Freiheit and Fabrice Zangl, "Model-based User-interface Management for Public Services," Electronic Journal of e-Government 5 (1), 53-62 (2007).
Abstract
Public business processes can be very complex. That makes it hard for citizens to understand these processes and for software companies to implement them into software tools. Changes of the process entail expensive effort in both teaching the citizens and adapting the software. For business processes several model-based approaches have been suggested to deal with high complexity, such as BPMN. However, modelling simplifies work of software developers rather than of citizens. We present an approach where an adequate user-interface with user-centric pertinent information is derived directly from the models. Our approach combines the advantages of having models for the software developers with the requirements of the users. The modelling technique we are using is Event-driven Process Chains (EPCs). EPCs are widely accepted in the commercial area and are comprehensively investigated in the academic area as well. Due to their graphical description they are easy to understand. EPCs are implemented in the ARIS toolset, which offers the possibility to attach attributes to the elements of the EPCs. This paper will demonstrate how these attributes are used to derive a user-interface, e.g. a relevant website or document, for each state or transition of the EPC. The tools used extract the values of the attributes and incorporate them into a web-based user-interface according to the EPC of the modelled business process. Execution of the model then is equivalent to running the user-interface. A change of the process requires a change of the model only, which is much easier to handle than changing the implementation of the user-interface.
Export
• Silvio Ghilardi, Ulrike Sattler, Viorica Sofronie-Stokkermans, and Ashish Tiwari (eds), Workshop Automated Deduction: Decidability, Complexity, Tractability (ADDCT'07). (n/a, Bremen, 2007).
Citation
Silvio Ghilardi, Ulrike Sattler, Viorica Sofronie-Stokkermans, and Ashish Tiwari (eds), Workshop Automated Deduction: Decidability, Complexity, Tractability (ADDCT'07). (n/a, Bremen, 2007).
Export
• Thomas Hillenbrand and Christoph Weidenbach, "Superposition for Finite Domains", in Max-Planck-Institut für Informatik / Research Report, (2007), pp. 25 p.
Citation
Thomas Hillenbrand and Christoph Weidenbach, "Superposition for Finite Domains", in Max-Planck-Institut für Informatik / Research Report, (2007), pp. 25 p.
Export
• Swen Jacobs and Uwe Waldmann, "Comparing Instance Generation Methods for Automated Reasoning," Journal of Automated Reasoning 38 (1/3), 57-78 (2007).
Citation
Swen Jacobs and Uwe Waldmann, "Comparing Instance Generation Methods for Automated Reasoning," Journal of Automated Reasoning 38 (1/3), 57-78 (2007).
Abstract
The clause-linking technique of Lee and Plaisted proves the unsatisfiability of a set of first-order clauses by generating a sufficiently large set of instances of these clauses that can be shown to be propositionally unsatisfiable. In recent years, this approach has been refined in several directions, leading to both tableau-based methods, such as the disconnection tableau calculus, and saturation-based methods, such as primal partial instantiation and resolution-based instance generation. We investigate the relationship between these calculi and answer the question to what extent refutation or consistency proofs in one calculus can be simulated in another one.
Export
• Swen Jacobs and Viorica Sofronie-Stokkermans, "Applications of hierarchical reasoning in the verification of complex systems," Electronic Notes in Theoretical Computer Science 174 (8), 39-54 (2007).
Citation
Swen Jacobs and Viorica Sofronie-Stokkermans, "Applications of hierarchical reasoning in the verification of complex systems," Electronic Notes in Theoretical Computer Science 174 (8), 39-54 (2007).
Abstract
In this paper we show how hierarchical reasoning can be used to verify properties of complex systems. Chains of local theory extensions are used to model a case study taken from the European Train Control System (ETCS) standard, but considerably simplified. We show how testing invariants and bounded model checking (for safety properties expressed by universally quantified formulae, depending on certain parameters of the systems) can automatically be reduced to checking satisfiability of ground formulae over a base theory.
Export
• Tal Lev-Ami, Christoph Weidenbach, Thomas Reps, and Mooly Sagiv, "Labelled Clauses", in Automated Deduction - CADE-21: 21st International Conference on Automated Deduction, edited by Frank Pfenning (Springer, Berlin, Germany, 2007), pp. 311-327.
Citation
Tal Lev-Ami, Christoph Weidenbach, Thomas Reps, and Mooly Sagiv, "Labelled Clauses", in Automated Deduction - CADE-21: 21st International Conference on Automated Deduction, edited by Frank Pfenning (Springer, Berlin, Germany, 2007), pp. 311-327.
Export
• Michel Ludwig and Uwe Waldmann, "An Extension of the Knuth-Bendix Ordering with LPO-like Properties", in Logic for Programming, Artificial Intelligence, and Reasoning: 14th International Conference, LPAR 2007, edited by Nachum Dershowitz and Andrei Voronkov (Springer, Berlin, Germany, 2007), pp. 348-362.
Citation
Michel Ludwig and Uwe Waldmann, "An Extension of the Knuth-Bendix Ordering with LPO-like Properties", in Logic for Programming, Artificial Intelligence, and Reasoning: 14th International Conference, LPAR 2007, edited by Nachum Dershowitz and Andrei Voronkov (Springer, Berlin, Germany, 2007), pp. 348-362.
Abstract
The Knuth-Bendix ordering is usually preferred over the lexicographic path ordering in successful implementations of resolution and superposition, but it is incompatible with certain requirements of hierarchic superposition calculi. Moreover, it does not allow non-linear definition equations to be oriented in a natural way. We present an extension of the Knuth-Bendix ordering that makes it possible to overcome these restrictions.
Export
• Christopher Lynch and Duc-Khanh Tran, "Automatic Decidability and Combinability Revisited", in Automated Deduction – CADE-21: 21st International Conference on Automated Deduction, edited by Frank Pfenning (Springer, Berlin, Germany, 2007), pp. 328-344.
Citation
Christopher Lynch and Duc-Khanh Tran, "Automatic Decidability and Combinability Revisited", in Automated Deduction – CADE-21: 21st International Conference on Automated Deduction, edited by Frank Pfenning (Springer, Berlin, Germany, 2007), pp. 328-344.
Export
• Silvio Ranise, Christophe Ringeissen, and Duc-Khanh Tran, "Combining Proof Producing Decision Procedures", in Frontiers of Combining Systems: 6th International Symposium, FroCoS 2007, edited by Frank Wolter (Springer, Germany, 2007), pp. 237-251.
Citation
Silvio Ranise, Christophe Ringeissen, and Duc-Khanh Tran, "Combining Proof Producing Decision Procedures", in Frontiers of Combining Systems: 6th International Symposium, FroCoS 2007, edited by Frank Wolter (Springer, Germany, 2007), pp. 237-251.
Export
• Andrey Rybalchenko and Viorica Sofronie-Stokkermans, "Constraint Solving for Interpolation", in Verification, Model Checking and Abstract Interpretation: 8th International Conference, VMCAI 2007, edited by Byron Cook and Andreas Podelski (Springer, Berlin, Germany, 2007), pp. 346-362.
Citation
Andrey Rybalchenko and Viorica Sofronie-Stokkermans, "Constraint Solving for Interpolation", in Verification, Model Checking and Abstract Interpretation: 8th International Conference, VMCAI 2007, edited by Byron Cook and Andreas Podelski (Springer, Berlin, Germany, 2007), pp. 346-362.
Abstract
Interpolation is an important component of recent methods for program verification. It provides a natural and effective means for computing separation between the sets of good' and bad' states. The existing algorithms for interpolant generation are proof-based: They require explicit construction of proofs, from which interpolants can be computed. Construction of such proofs is a difficult task. We propose an algorithm for the generation of interpolants for the combined theory of linear arithmetic and uninterpreted function symbols that does not require a priori constructed proofs to derive interpolants. It uses a reduction of the problem to constraint solving in linear arithmetic, which allows application of existing highly optimized Linear Programming solvers in black-box fashion. We provide experimental evidence of the practical applicability of our algorithm.
Export
• Viorica Sofronie-Stokkermans, "On unification in certain finitely generated varieties of algebras", in Proceedings of the 21th International Workshop on Unification (UNIF 2007), edited by Evelyne Contejean (INRIA, [s.l.], 2007), pp. 1-5.
Citation
Viorica Sofronie-Stokkermans, "On unification in certain finitely generated varieties of algebras", in Proceedings of the 21th International Workshop on Unification (UNIF 2007), edited by Evelyne Contejean (INRIA, [s.l.], 2007), pp. 1-5.
Export
• Viorica Sofronie-Stokkermans, "On unification for bounded distributive lattices," ACM Transactions on Computational Logic 8 (2), 12.1-12.28 (2007).
Citation
Viorica Sofronie-Stokkermans, "On unification for bounded distributive lattices," ACM Transactions on Computational Logic 8 (2), 12.1-12.28 (2007).
Abstract
We give a method for deciding unifiability in the variety of bounded distributive lattices. For this, we reduce the problem of deciding whether a unification problem ${\cal S}$ has a solution to the problem of checking the satisfiability of a set $\Phi_{\cal S}$ of ground clauses. This is achieved by using a structure-preserving translation to clause form. The satisfiability check can then be performed either by a resolution-based theorem prover or by a SAT checker. We apply the method to unification with free constants and to unification with linear constant restrictions, and show that, in fact, it yields a decision procedure for the positive theory of the variety of bounded distributive lattices. We also consider the problem of unification over (i.e.\ in an algebraic extension of) the free lattice. Complexity issues are also addressed.
Export
• Viorica Sofronie-Stokkermans and Carsten Ihlemann, "Automated reasoning in some local extensions of ordered structures," Journal of Multiple-Valued Logic and Soft Computing 13 (4-6), 397-414 (2007).
Citation
Viorica Sofronie-Stokkermans and Carsten Ihlemann, "Automated reasoning in some local extensions of ordered structures," Journal of Multiple-Valued Logic and Soft Computing 13 (4-6), 397-414 (2007).
Abstract
We give a uniform method for automated reasoning in several types of extensions of ordered algebraic structures (definitional extensions, extensions with boundedness axioms or with monotonicity axioms). We show that such extensions are local and, hence, efficient methods for hierarchical reasoning exist in all these cases.
Export
• Viorica Sofronie-Stokkermans and Carsten Ihlemann, "Automated reasoning in some local extensions of ordered structures", in Proceedings of the 37th International Symposium on Multiple-Valued Logic (ISMVL'07), (IEEE Computer Society, Los Alamitos, CA, USA, 2007), pp. p.1.1-6.
Citation
Viorica Sofronie-Stokkermans and Carsten Ihlemann, "Automated reasoning in some local extensions of ordered structures", in Proceedings of the 37th International Symposium on Multiple-Valued Logic (ISMVL'07), (IEEE Computer Society, Los Alamitos, CA, USA, 2007), pp. p.1.1-6.
Abstract
We give a uniform method for automated reasoning in several types of extensions of ordered algebraic structures (definitional extensions, extensions with boundedness axioms or with monotonicity axioms). We show that such extensions are local and, hence, efficient methods for hierarchical reasoning exist in all these cases.
Export
• Viorica Sofronie-Stokkermans, "Automated theorem proving by resolution in non-classical logics," Annals of Mathematics and Artificial Intelligence 49 (1-4), 221-252 (2007).
Citation
Viorica Sofronie-Stokkermans, "Automated theorem proving by resolution in non-classical logics," Annals of Mathematics and Artificial Intelligence 49 (1-4), 221-252 (2007).
Abstract
This paper is an overview of a variety of results, all centered around a common theme, namely embedding of non-classical logics into first order logic and resolution theorem proving. We present several classes of non-classical logics, many of which are of great practical relevance in knowledge representation, which can be translated into tractable and relatively simple fragments of classical logic. In this context, we show that refinements of resolution can often be used successfully for automated theorem proving, and in many interesting cases yield optimal decision procedures.
Export
• Viorica Sofronie-Stokkermans, Carsten Ihlemann, and Swen Jacobs, "Local Theory Extensions, Hierarchical Reasoning and Applications to Verification", in Deduction and Decision Procedures, edited by Franz Baader, Byron Cook, Jürgen Giesl, and Robert Nieuwenhuis (IBFI, Dagstuhl, Germany, 2007), pp. 1-22.
Citation
Viorica Sofronie-Stokkermans, Carsten Ihlemann, and Swen Jacobs, "Local Theory Extensions, Hierarchical Reasoning and Applications to Verification", in Deduction and Decision Procedures, edited by Franz Baader, Byron Cook, Jürgen Giesl, and Robert Nieuwenhuis (IBFI, Dagstuhl, Germany, 2007), pp. 1-22.
Abstract
Many problems occurring in verification can be reduced to proving the satisfiability of conjunctions of literals in a background theory. This can be a concrete theory (e.g. the theory of real or rational numbers), the extension of a theory with additional functions (free, monotone, or recursively defined) or a combination of theories. It is therefore very important to have efficient procedures for checking the satisfiability of conjunctions of ground literals in such theories. We present some new results on hierarchical and modular reasoning in complex theories, as well as several examples of application domains in which efficient reasoning is possible. We show, in particular, that various phenomena analyzed in the verification literature can be explained in a unified way using the notion of local theory extension.
Export
• Viorica Sofronie-Stokkermans, "Hierarchical and modular reasoning in complex theories: The case of local theory extensions", in Frontiers of Combining Systems: 6th International Symposium, FroCos 2007, edited by Boris Konev and Frank Wolter (Springer, Berlin, Germany, 2007), pp. 47-71.
Citation
Viorica Sofronie-Stokkermans, "Hierarchical and modular reasoning in complex theories: The case of local theory extensions", in Frontiers of Combining Systems: 6th International Symposium, FroCos 2007, edited by Boris Konev and Frank Wolter (Springer, Berlin, Germany, 2007), pp. 47-71.
Abstract
Many problems in computer science can be reduced to proving the satisfiability of conjunctions of literals w.r.t. a background theory. This theory can be a concrete theory (e.g. the theory of real or rational numbers), the extension of a theory with additional functions (free, monotone, or recursively defined) or a combination of theories. It is therefore very important to have efficient procedures for checking the satisfiability of conjunctions of ground literals in such theories. We here give an overview of results on hierarchical and modular reasoning in complex theories. We show that for a special type of extensions of a base theory, which we call local, hierarchic reasoning is possible (i.e. proof tasks in the extension can be hierarchically reduced to proof tasks w.r.t. the base theory). Many theories important for computer science or mathematics fall into this class (typical examples are theories of data structures, theories of free or monotone functions, but also functions occurring in mathematical analysis). In fact, it is often necessary to consider complex extensions, in which various types of functions or data structures need to be taken into account at the same time. We show how such local theory extensions can be identified and under which conditions locality is preserved when combining theories, and we investigate possibilities of efficient modular reasoning in such theory combinations. We present several examples of application domains where such theories occur in a natural way. We show, in particular, that various phenomena analyzed in the verification literature can be explained in a unified way using the notion of locality.
Export
• Viorica Sofronie-Stokkermans, "Algebraic and logical methods in computer science: some aspects", in Grigore C. Moisil and his followers, edited by Afrodita Iorgulescu, Solomon Marcus, Sergiu Rudeanu, and Dragos Vaida (Editura Academiei Romane, Bucharest, Romania, 2007), pp. 488-493.
Citation
Viorica Sofronie-Stokkermans, "Algebraic and logical methods in computer science: some aspects", in Grigore C. Moisil and his followers, edited by Afrodita Iorgulescu, Solomon Marcus, Sergiu Rudeanu, and Dragos Vaida (Editura Academiei Romane, Bucharest, Romania, 2007), pp. 488-493.
Export
• Duc-Khanh Tran, Conception de Procedures de Decision par Combinaison et Saturation, PhD Thesis, Université Henri Poincaré, 2007.
Citation
Duc-Khanh Tran, Conception de Procedures de Decision par Combinaison et Saturation, PhD Thesis, Université Henri Poincaré, 2007.
Export
• Christoph Weidenbach, Renate Schmidt, Thomas Hillenbrand, Rostislav Rusev, and Dalibor Topic, "System Description: Spass Version 3.0", in Automated Deduction - CADE-21, edited by Frank Pfenning (Springer, Berlin, 2007), pp. 514-520.
Citation
Christoph Weidenbach, Renate Schmidt, Thomas Hillenbrand, Rostislav Rusev, and Dalibor Topic, "System Description: Spass Version 3.0", in Automated Deduction - CADE-21, edited by Frank Pfenning (Springer, Berlin, 2007), pp. 514-520.
Export
• Patrick Wischnewski, Contextual Rewriting in SPASS, Master Thesis, Universität des Saarlandes, 2007.
Citation
Patrick Wischnewski, Contextual Rewriting in SPASS, Master Thesis, Universität des Saarlandes, 2007.
Abstract
First-order theorem proving with equality is undecidable, in general. However, it is semi-decidable in the sense that it is refutationally complete. The basis for a (semi)-decision procedure for first-order clauses with equality is a calculus composed of inference and reduction rules. The inference rules of the calculus generate new clauses whereas the reduction rules delete clauses or transform them into simpler ones. If, in particular, strong reduction rules are available, decidability of certain subclasses of first-order logic can be shown. Hence, sophisticated reductions are essential for progress in automated theorem proving. In this thesis we consider the superposition calculus and in particular the sophisticated reduction rule Contextual Rewriting. However, it is in general undecidable whether contextual rewriting can be applied. Therefore, to make the rule applicable in practice, it has to be further refined. In this work we develop an instance of contextual rewriting which effectively performs contextual rewriting and we implement this in the theorem prover Spass.
Export
• Joerg Ziemann, Thomas Matheis, and Jörn Freiheit, "Modelling of Cross-Organizational Business Processes", in EMISA 2007: enterprise modelling and information systems architectures; concepts and architectures, edited by Manfred Reichert (Gesellschaft fuer Informatik, Bonn, Germany, 2007), pp. 87-95.
Citation
Joerg Ziemann, Thomas Matheis, and Jörn Freiheit, "Modelling of Cross-Organizational Business Processes", in EMISA 2007: enterprise modelling and information systems architectures; concepts and architectures, edited by Manfred Reichert (Gesellschaft fuer Informatik, Bonn, Germany, 2007), pp. 87-95.
Export
• Joerg Ziemann, Thomas Matheis, and Jörn Freiheit, "Modelling of Cross-Organizational Business Processes - Current Methods and Standards," Enterprise Modelling and Information Systems Architectures 2 (2), 23-31 (2007).
Citation
Joerg Ziemann, Thomas Matheis, and Jörn Freiheit, "Modelling of Cross-Organizational Business Processes - Current Methods and Standards," Enterprise Modelling and Information Systems Architectures 2 (2), 23-31 (2007).
Abstract
Not only since the upcoming of Service-oriented Architectures the modelling of cross-organizational business processes is a heavily investigated field comprising dozens of standards based on different concepts. New techniques on the implementation site, e.g. Web Service orchestration and choreography, further extended the possibilities and requirements on such standards. To systematically order and present a comprehensive state of the art of relevant methods and standards this paper first describes requirements that occur in cross-organizational business processes both for concepts and modelling languages. Then the most important state of the art concepts for modelling cross-organizational processes are described. Based on the requirements defined before and the presented concepts, selected modelling languages are analysed.
Export
• Stephan Zimmer, Intelligent Combination of a First Order Theorem Prover and SMT Procedures, Diploma Thesis, Universität des Saarlandes, 2007.
Citation
Stephan Zimmer, Intelligent Combination of a First Order Theorem Prover and SMT Procedures, Diploma Thesis, Universität des Saarlandes, 2007.
Abstract
First-order logic combined with arithmetic background theories is a powerful tool for representing and managing huge amounts of declarative information. Special fragments of it were successfully applied to manifold problems from different areas of computer science. From an automated reasoning perspective, however, this expressiveness makes it particular challenging to develop theorem provers that can deal with general classes of those languages: General purpose theorem provers on the one hand cannot cope efficiently with arithmetic and specialized decision procedures on the other hand are notoriously bad at dealing with quantifiers, if they are even supported at all. The SPASS+T system, which was developed by Prevosto and Waldmann, aims to attack this problem by combining the superposition-based theorem prover SPASS with decision procedures for linear arithmetic and free function symbols; furthermore, the set of standard first-order inference and reduction rules is complemented by specialized rules for arithmetic. In this work we present various extensions to their initial implementation. The main task of the thesis was to stretch the capabilities of the system by integrating the SPASS splitting rule, which had to be switched off so far. Splitting is highly efficient for SPASS and has also advantages in a combination like SPASS+T. In order to add support for splitting in SPASS+T we first revised the previous system architecture and developed an advanced coupling between SPASS and the SMT procedure and achieved a tighter integration of the latter in form of a new inference rule. Furthermore, for splitting a careful analysis of the different prover configurations was necessary. Besides splitting, the new coupling also allows to use the SPASS proof documentation mode regarding subproofs that were contributed by the SMT procedure. The documented proofs can be automatically certified. To this end we extended the existing SPASS proof validator in such a way that it also employs an external SMT procedure and now can verify, besides ordinary first-order proof steps, arithmetic inferences as well. In order to improve the built-in arithmetic simplification rules of SPASS+T and let them also work with bignums and rational numbers, we integrated the GNU multiple precision library. Finally, we added a new reduction rule that deals with clauses which impose lower or upper bounds on a variable. We will describe all these extensions in detail, discuss their impact on the system architecture, and demonstrate the capabilities of the system by applying it to some examples.
Export
• Jan Bankstahl, Netflow analysis of SAP R/3 traffic in an enterprise environment, Diploma Thesis, Universität des Saarlandes, 2006.
Citation
Jan Bankstahl, Netflow analysis of SAP R/3 traffic in an enterprise environment, Diploma Thesis, Universität des Saarlandes, 2006.
Export
• Andrea Bastuck, Maschinell unterstützte Analyse eines Sicherheitsprotokolls, Diploma Thesis, Universität des Saarlandes, 2006.
Citation
Andrea Bastuck, Maschinell unterstützte Analyse eines Sicherheitsprotokolls, Diploma Thesis, Universität des Saarlandes, 2006.
Export
• Werner Damm, Stefan Disch, Hardi Hungar, Jun Pang, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, and Boris Wirtz, "Automatic Verification of Hybrid Systems with Large Discrete State Space", in Automated Technology for Verification and Analysis, 4th International Symposium, ATVA 2006, edited by Susanne Graf and Wenhui Zhang (Springer, Berlin, Germany, 2006), pp. 276-291.
Citation
Werner Damm, Stefan Disch, Hardi Hungar, Jun Pang, Florian Pigorsch, Christoph Scholl, Uwe Waldmann, and Boris Wirtz, "Automatic Verification of Hybrid Systems with Large Discrete State Space", in Automated Technology for Verification and Analysis, 4th International Symposium, ATVA 2006, edited by Susanne Graf and Wenhui Zhang (Springer, Berlin, Germany, 2006), pp. 276-291.
Abstract
We address the problem of model checking hybrid systems which exhibit nontrivial discrete behavior and thus cannot be treated by considering the discrete states one by one, as most currently available verification tools do. Our procedure relies on a deep integration of several techniques and tools. An extension of AND-Inverter-Graphs (AIGs) with first-order constraints serves as a compact representation format for sets of configurations which are composed of continuous regions and discrete states. Boolean reasoning on the AIGs is complemented by firstorder reasoning in various forms and on various levels. These include implication checks for simple constraints, test vector generation for fast inequality checks of boolean combinations of constraints, and an exact subsumption check for representations of two configurations.\par These techniques are integrated within a model checker for universal CTL. Technically, it deals with discrete-time hybrid systems with linear differentials. The paper presents the approach, its prototype implementation, and first experimental data.
Export
• Jörn Freiheit, Marc Luuk, Susanne Münch, Grozdana Sijanski, and Fabrice Zangl, "Lexecute: Visualisation and representation of legal procedures," Digital Evidence Journal 3 (1), 17-27 (2006).
Citation
Jörn Freiheit, Marc Luuk, Susanne Münch, Grozdana Sijanski, and Fabrice Zangl, "Lexecute: Visualisation and representation of legal procedures," Digital Evidence Journal 3 (1), 17-27 (2006).
Export
• Jörn Freiheit and Fabrice Zangl, "Model-based user-interface management for public services", in 6th European Conference on e-Government, (Academic Conferences Limited, Reading, UK, 2006), pp. 141-151.
Citation
Jörn Freiheit and Fabrice Zangl, "Model-based user-interface management for public services", in 6th European Conference on e-Government, (Academic Conferences Limited, Reading, UK, 2006), pp. 141-151.
Export
• Harald Ganzinger, Viorica Sofronie-Stokkermans, and Uwe Waldmann, "Modular Proof Systems for Partial Functions with Evans Equality," Information and Computation 204 (10), 1453-1492 (2006).
Citation
Harald Ganzinger, Viorica Sofronie-Stokkermans, and Uwe Waldmann, "Modular Proof Systems for Partial Functions with Evans Equality," Information and Computation 204 (10), 1453-1492 (2006).
Abstract
The paper presents a modular superposition calculus for the combination of first-order theories involving both total and partial functions. Modularity means that inferences are pure, only involving clauses over the alphabet of either one, but not both, of the theories. The calculus is shown to be complete provided that functions that are not in the intersection of the component signatures are declared as partial. This result also means that if the unsatisfiability of a goal modulo the combined theory does not depend on the totality of the functions in the extensions, the inconsistency will be effectively found. Moreover, we consider a constraint superposition calculus for the case of hierarchical theories and show that it has a related modularity property. Finally we identify cases where the partial models can always be made total so that modular superposition is also complete with respect to the standard (total function) semantics of the theories.
Export
• Thomas Hillenbrand, Dalibor Topic, and Christoph Weidenbach, "Sudokus as Logical Puzzles", in Disproving'06: Non-Theorems, Non-Validity, Non-Provability, edited by Hans de Nivelle (Self publishing, Seattle, USA, 2006), pp. 2-12.
Citation
Thomas Hillenbrand, Dalibor Topic, and Christoph Weidenbach, "Sudokus as Logical Puzzles", in Disproving'06: Non-Theorems, Non-Validity, Non-Provability, edited by Hans de Nivelle (Self publishing, Seattle, USA, 2006), pp. 2-12.
Export
• Swen Jacobs and Viorica Sofronie-Stokkermans, "Applications of hierarchical reasoning in the verification of complex systems", in PDPAR'06: Pragmatical Aspects of Decision Procedures in Automated Reasoning, edited by Byron Cook and Roberto Sebastiani (2006), pp. 15-26.
Citation
Swen Jacobs and Viorica Sofronie-Stokkermans, "Applications of hierarchical reasoning in the verification of complex systems", in PDPAR'06: Pragmatical Aspects of Decision Procedures in Automated Reasoning, edited by Byron Cook and Roberto Sebastiani (2006), pp. 15-26.
Abstract
In this paper we show how hierarchical reasoning can be used to verify properties of complex systems. Chains of local theory extensions are used to model a case study taken from the European Train Control System (ETCS) standard, but considerably simplified. We show how testing invariants and bounded model checking can automatically be reduced to checking satisfiability of ground formulae over a base theory.
Export
• Yevgeny Kazakov, Saturation-Based Decision Procedures For Extensions Of The Guarded Fragment, PhD Thesis, Universität des Saarlandes, 2006.
Citation
Yevgeny Kazakov, Saturation-Based Decision Procedures For Extensions Of The Guarded Fragment, PhD Thesis, Universität des Saarlandes, 2006.
Abstract
We apply the framework of Bachmair and Ganzinger for saturation-based theorem proving to derive a range of decision procedures for logical formalisms, starting with a simple terminological language EL, which allows for conjunction and existential restrictions only, and ending with extensions of the guarded fragment with equality, constants, functionality, number restrictions and compositional axioms of form S ◦ T Í H. Our procedures are derived in a uniform way using standard saturation-based calculi enhanced with simplication rules based on the general notion of redundancy. We argue that such decision procedures can be applied for reasoning in expressive description logics, where they have certain advantages over traditionally used tableau procedures, such as optimal worst-case complexity and direct correctness proofs.
Export
• Nimrod Lilith, Jonathan Billington, and Jörn Freiheit, "Approximate Closed-Form Aggregation of a Fork-Join Structure in Generalised Stochastic Petri Nets", in Proceedings of the 1st International Conference on Performance Evaluation Methodolgies and Tools, VALUETOOLS 2006, edited by Luciano Lenzini and Rene L. Cruz (ACM, New York, USA, 2006), pp. 1-10.
Citation
Nimrod Lilith, Jonathan Billington, and Jörn Freiheit, "Approximate Closed-Form Aggregation of a Fork-Join Structure in Generalised Stochastic Petri Nets", in Proceedings of the 1st International Conference on Performance Evaluation Methodolgies and Tools, VALUETOOLS 2006, edited by Luciano Lenzini and Rene L. Cruz (ACM, New York, USA, 2006), pp. 1-10.
Abstract
In this paper an aggregation technique for generalised stochastic Petri nets (GSPNs) possessing synchronised parallel structures is presented. Parallel processes featuring synchronisation constraints commonly occur in fields such as product assembly and computer process communications, however their existence in closed networks severely complicates analysis. This paper details the derivation of computationally-simple closed-form expressions which permit the aggregation of a GSPN subnet featuring a fork-join structure. The aggregation expressions presented in this paper do not require the generation of the underlying continuous time Markov chain of the original net, and do not follow an iterative procedure. The resulting aggregated GSPN accurately approximates the stationary token distribution behaviour of the original net, and this is shown by the analysis of a number of example GSPNs.
Export
• Carlo Simon, Jörn Freiheit, and Sebastian Olbrich, "Using BPEL processes defined by Event-driven Process Chains", in 5. GI-Workshop "EPK 2006 - Geschäftsprozessmanagement mit Ereignisgesteuerten Prozessketten", edited by Markus Nüttgens, Frank J. Rump, and Jan Mendling (CEUR Workshop Proceedings, Aachen, Germany, 2006), pp. 121-135.
Citation
Carlo Simon, Jörn Freiheit, and Sebastian Olbrich, "Using BPEL processes defined by Event-driven Process Chains", in 5. GI-Workshop "EPK 2006 - Geschäftsprozessmanagement mit Ereignisgesteuerten Prozessketten", edited by Markus Nüttgens, Frank J. Rump, and Jan Mendling (CEUR Workshop Proceedings, Aachen, Germany, 2006), pp. 121-135.
Export
• Viorica Sofronie-Stokkermans, "Local reasoning in verification", in IJCAR'06 Workshop: VERIFY'06: Verification Workshop, edited by Serge Autexier and Heiko Mantel (-, -, 2006), pp. 128-145.
Citation
Viorica Sofronie-Stokkermans, "Local reasoning in verification", in IJCAR'06 Workshop: VERIFY'06: Verification Workshop, edited by Serge Autexier and Heiko Mantel (-, -, 2006), pp. 128-145.
Abstract
The goal of this paper is to illustrate the wide applicability in verification of results on local reasoning, and especially on hierarchical reasoning in local theory extensions. The paper contains a survey of our results on reasoning in local theory extensions, ranging from characterizations of locality to interpolation. In addition, several examples are provided, emphasizing theories occurring in a natural way in verification. We give several examples -- some already existing in the literature, others obtained during the work in the AVACS project -- of application domains where such theories occur in a natural way.
Export
• Viorica Sofronie-Stokkermans, "Interpolation in local theory extensions", in Proceedings of IJCAR 2006, edited by Ulrich Furbach and Natarajan Shankar (Springer, New York, 2006), pp. 235-250.
Citation
Viorica Sofronie-Stokkermans, "Interpolation in local theory extensions", in Proceedings of IJCAR 2006, edited by Ulrich Furbach and Natarajan Shankar (Springer, New York, 2006), pp. 235-250.
Abstract
Many problems in mathematics and computer science (e.g. in verification, or when reasoning in and about distributed databases) can be reduced to proving the satisfiability of conjunctions of (ground) literals modulo a background theory. This theory can, for instance, be the extension of a base theory with additional functions or a combination of theories. It is therefore very important to find efficient methods for checking the unsatisfiability of ground formulae in such complex theories. However, it is often equally important to find local causes for inconsistency. Such information is usually provided by interpolants. In this paper we study interpolation in local extensions of a base theory ${\cal T}_0$. In such extensions efficient hierarchical reasoning -- in which a prover for the base theory is used as a black box -- is possible. We identify situations in which it is possible to obtain interpolants in a hierarchical manner, by using a prover and a procedure for generating interpolants in ${\cal T}_0$ as `black-boxes' in order to generate interpolants in the extension. We provide several examples of such theories, and discuss their applications in verification or knowledge representation.
Export
• Viorica Sofronie-Stokkermans, "Sheaves and geometric logic in concurrency", in Proceedings of the Eighth Workshop on Geometric and Topological Methods in Concurrency (GETCO 2006), (-, -, 2006).
Citation
Viorica Sofronie-Stokkermans, "Sheaves and geometric logic in concurrency", in Proceedings of the Eighth Workshop on Geometric and Topological Methods in Concurrency (GETCO 2006), (-, -, 2006).
Abstract
In this paper we present an overview of results that show that states, transitions and behavior of concurrent systems can often be modeled as sheaves over a suitable topological space. In such contexts, geometric logic can be used to test whether (and describe which) local properties, of individual systems, are preserved, at a global level, when interconnecting the systems.
Export
• Viorica Sofronie-Stokkermans, "Automatisches Beweisen in komplexen Theorien," Jahrbuch der Max-Planck-Gesellschaft - (2006).
Citation
Viorica Sofronie-Stokkermans, "Automatisches Beweisen in komplexen Theorien," Jahrbuch der Max-Planck-Gesellschaft - (2006).
Abstract
Wir erforschen Rahmenbedingungen, die es ermöglichen, Beweisaufgaben in komplexen Theorien modular in Beweisaufgaben für die einfacheren Bestandteile dieser Theorien zu zerlegen. Durch Ausnutzung der Modularität sind solche Beweisverfahren besonders flexibel und effizient und deshalb in vielen Bereichen (wie etwa in der Verifikation komplexer Systeme, aber auch in der Mathematik oder Wissensrepräsentation) anwendbar.
Export
• Nicolas Cuntz, Jörn Freiheit, and Ekkart Kindler, "On the semantics of EPCs: Faster calculation for EPCs with small state spaces", in EPK 2005. 4. Workshop der GI, Arbeitskreis: Geschäftsprozessmanagement mit Ereignisgesteuerten Prozessketten, (Gesellschaft für Informatik, Bonn, Germany, 2005), pp. 7-23.
Citation
Nicolas Cuntz, Jörn Freiheit, and Ekkart Kindler, "On the semantics of EPCs: Faster calculation for EPCs with small state spaces", in EPK 2005. 4. Workshop der GI, Arbeitskreis: Geschäftsprozessmanagement mit Ereignisgesteuerten Prozessketten, (Gesellschaft für Informatik, Bonn, Germany, 2005), pp. 7-23.
Export
• Matthias Daum, Stefan Maus, Norbert Schirmer, and Mohammed Nassim Seghir, "Integration of a Software Model Checker into Isabelle", in Logic for Programming, Artificial Intelligence, and Reasoning: 12th International Conference, LPAR 2005, (Springer, Berlin, Germany, 2005), pp. 381-395.
Citation
Matthias Daum, Stefan Maus, Norbert Schirmer, and Mohammed Nassim Seghir, "Integration of a Software Model Checker into Isabelle", in Logic for Programming, Artificial Intelligence, and Reasoning: 12th International Conference, LPAR 2005, (Springer, Berlin, Germany, 2005), pp. 381-395.
Abstract
The paper presents a combination of interactive and automatic tools in the area of software verification. We have integrated a newly developed software model checker into an interactive verification environment for imperative programming languages. Although the problems in software verification are mostly too hard for full automation, we could increase the level of automated assistance by discharging less interesting side conditions. That allows the verification engineer to focus on the abstract algorithm, safely assuming unbounded arithmetic and unlimited buffers.
Export
• Jörn Freiheit, Susanne Münch, Hendrik Schöttle, Grozdana Sijanski, and Fabrice Zangl, "Enhanced Workflow Models as a Tool for Judicial Practitioners", in On the move to meaningful internet systems 2005: OTM 2005 Workshops: OTM Confederated International Workshops and Posters, AWeSOMe, CAMS, GADA, MIOS+INTEROP, ORM, PhDS, SeBGIS, SWWS, and WOSE 2005, (Springer, Berlin, Germany, 2005), pp. 26-27.
Citation
Jörn Freiheit, Susanne Münch, Hendrik Schöttle, Grozdana Sijanski, and Fabrice Zangl, "Enhanced Workflow Models as a Tool for Judicial Practitioners", in On the move to meaningful internet systems 2005: OTM 2005 Workshops: OTM Confederated International Workshops and Posters, AWeSOMe, CAMS, GADA, MIOS+INTEROP, ORM, PhDS, SeBGIS, SWWS, and WOSE 2005, (Springer, Berlin, Germany, 2005), pp. 26-27.
Abstract
In the past, attempts were made to make law and justice more accessible to general audience and to legal practitioners using models of legal texts. We present a new approach to make the judicial workflows easier to understand. By using process modelling methods, the developed representation emphasises on improving transparency, on promoting mutual trust and on formalising models for verification. To design semi-formal models interviews are used as well as legal texts are consulted. These models are formalised in a second step. The models are enhanced with hierarchies, modules and the generation of different views. Language problems are also treated. The subsequent formalised models are used to verify trigger events and timing of judicial workflows, which have very specific requirements in terms of periods of time and fixed dates. A new tool, Lexecute, is presented which gives new perspectives into justice and reveal new potentials for modelling methods in the field of justice.
Export
• Swen Jacobs and Uwe Waldmann, "Comparing Instance Generation Methods for Automated Reasoning", in Automated Reasoning with Analytic Tableaux and Related Methods: International Conference, TABLEAUX 2005, edited by Bernhard Beckert (Springer, Berlin, Germany, 2005), pp. 153-168.