| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Chris Hawblitzel, Ming Kawaguchi, Shuvendu K. Lahiri, Henrique Rebêlo |
Towards Modularly Comparing Programs Using Automated Theorem Provers.  |
CADE  |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Noran Azmy, Christoph Weidenbach |
Computing Tiny Clause Normal Forms. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Bernhard Beckert, Rajeev Goré, Carsten Schürmann 0001 |
Analysing Vote Counting Algorithms via Logic - And Its Application to the CADE Election Scheme. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Kühlwein, Stephan Schulz 0001, Josef Urban |
E-MaLeS 1.1. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Jasmin Christian Blanchette, Andrei Paskevich |
TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Hubert Comon-Lundh, Véronique Cortier, Guillaume Scerri |
Tractable Inference Systems: An Extension with a Deducibility Predicate. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Jean-Christophe Filliâtre |
One Logic to Use Them All. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Koen Claessen, Moa Johansson, Dan Rosén, Nicholas Smallbone |
Automating Inductive Proofs Using Theory Exploration. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Maria Paola Bonacina (eds.) |
Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Reiner Hähnle, Ina Schaefer, Richard Bubel |
Reuse in Software Verification by Abstract Method Calls. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Leonardo Mendonça de Moura, Grant Olney Passmore |
Computation in Real Closed Infinitesimal and Transcendental Extensions of the Rationals. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar |
Automated Reasoning, Fast and Slow. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Marijn Heule, Warren A. Hunt Jr., Nathan Wetzler |
Verifying Refutations with Extended Resolution. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Serdar Erbatur, Deepak Kapur, Andrew M. Marshall, Paliath Narendran, Christophe Ringeissen |
Hierarchical Combination. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Ulrich Loup, Karsten Scheibler, Florian Corzilius, Erika Ábrahám, Bernd Becker 0001 |
A Symbiosis of Interval Constraint Propagation and Cylindrical Algebraic Decomposition. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Sicun Gao, Soonho Kong, Edmund M. Clarke |
dReal: An SMT Solver for Nonlinear Theories over the Reals. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Goré, Jimmy Thomson 0001 |
An Improved BDD Method for Intuitionistic Propositional Logic: BDDIntKt System Description. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Abdelkader Kersani, Nicolas Peltier |
Completeness and Decidability Results for First-Order Clauses with Indices. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Gergely Kovásznai, Andreas Fröhlich, Armin Biere |
: A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Baumgartner 0001, Uwe Waldmann |
Hierarchic Superposition with Weak Abstraction. |
CADE |
2013 |
DBLP DOI BibTeX RDF |
|
| 1 | Pavel Klinov, Bijan Parsia |
A Hybrid Method for Probabilistic Satisfiability. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Konstantin Korovin, Andrei Voronkov |
Solving Systems of Linear Inequalities by Bound Propagation. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Koen Claessen |
The Anatomy of Equinox - An Extensible Automated Reasoning Tool for First-Order Logic and Beyond - (Talk Abstract). |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Nikolaj S. Bjørner, Viorica Sofronie-Stokkermans (eds.) |
Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Matthew Fredrikson, Mihai Christodorescu, Somesh Jha |
Dynamic Behavior Matching: A Complexity Analysis and New Approximation Algorithms. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Aarne Ranta |
Translating between Language and Logic: What Is Easy and What Is Difficult. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Chad E. Brown |
Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Matthias Horbach |
System Description: SPASS-FD. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Koen Claessen, Ann Lillieström, Nicholas Smallbone |
Sort It Out with Monotonicity - Translating between Many-Sorted and Unsorted First-Order Logic. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Armin Biere, Florian Lonsing, Martina Seidl |
Blocked Clause Elimination for QBF. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Zhiqiang Liu, Christopher Lynch |
Efficient General Unification for XOR with Homomorphism. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Ali Sinan Köksal, Viktor Kuncak, Philippe Suter |
Scala to the Power of Z3: Integrating SMT and Programming. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Étienne Payet, Fausto Spoto |
Static Analysis of Android Programs. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | James Brotherston, Dino Distefano, Rasmus Lerchedahl Petersen |
Automated Cyclic Entailment Proofs in Separation Logic. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | André Platzer |
Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Mathilde Arnaud, Véronique Cortier, Stéphanie Delaune |
Deciding Security for Protocols with Recursive Tests. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Byron Cook |
Advances in Proving Program Termination and Liveness. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Matthias Horbach |
Predicate Completion for non-Horn Clause Sets. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Sarah Winkler, Aart Middeldorp |
AC Completion with Termination Tools. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Didier Galmiche, Daniel Méry |
A Connection-Based Characterization of Bi-intuitionistic Validity. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Laura Kovács, Georg Moser, Andrei Voronkov |
On Transfinite Knuth-Bendix Orders. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Thomas Wies, Marco Muñiz, Viktor Kuncak |
An Efficient Decision Procedure for Imperative Tree Data Structures. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Krystof Hoder, Andrei Voronkov |
Sine Qua Non for Large Theory Reasoning. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Jasmin Christian Blanchette, Sascha Böhme, Lawrence C. Paulson |
Extending Sledgehammer with SMT Solvers. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Volker Haarslev, Roberto Sebastiani, Michele Vescovi |
Automated Reasoning in ALCQ\mathcal{ALCQ} via SMT. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Sascha Böhme, Michal Moskal |
Heaps and Data Structures: A Challenge for Automated Provers. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Francesco Alberti, Alessandro Armando, Silvio Ranise |
ASASP: Automated Symbolic Analysis of Security Policies. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael Schneider 0001, Geoff Sutcliffe |
Reasoning in the OWL 2 Full Ontology Language Using First-Order Automated Theorem Proving. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Alexandros Chortaras, Despoina Trivela, Giorgos B. Stamou |
Optimized Query Rewriting for OWL 2 QL. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo |
Compression of Propositional Resolution Proofs via Partial Regularization. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Baumgartner 0001, Cesare Tinelli |
Model Evolution with Equality Modulo Built-in Theories. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | David Déharbe, Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo |
Exploiting Symmetry in SMT Problems. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Dejan Jovanovic, Leonardo Mendonça de Moura |
Cutting to the Chase Solving Linear Integer Arithmetic. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Harald Zankl, Bertram Felgenhauer, Aart Middeldorp |
CSI - A Confluence Tool. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Noschinski, Fabian Emmes, Jürgen Giesl |
A Dependency Pair Framework for Innermost Complexity Analysis of Term Rewrite Systems. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Guillaume Burel |
Experimenting with Deduction Modulo. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | María Alpuente, Demis Ballis, Javier Espert, Daniel Romero 0001 |
Backward Trace Slicing for Rewriting Logic Theories. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Franz Baader, Thanh Binh Nguyen 0003, Stefan Borgwardt, Barbara Morawska 0001 |
Unification in the Description Logic EL without the Top Concept. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi |
The Matita Interactive Theorem Prover. |
CADE |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Shuvendu K. Lahiri, Shaz Qadeer |
Complexity and Algorithms for Monomial and Clausal Predicate Abstraction. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Mark E. Stickel |
Building Theorem Provers. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Amit Goel, Sava Krstic, Cesare Tinelli |
Ground Interpolation for Combined Theories. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Enrica Nicolini, Christophe Ringeissen, Michaël Rusinowitch |
Combinable Extensions of Abelian Groups. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Alex Roederer, Yury Puzis, Geoff Sutcliffe |
Divvy: An ATP Meta-system Based on Axiom Relevance Ordering. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Jörg Endrullis, Clemens Grabmayer, Dimitri Hendriks |
Complexity of Fractran and Productivity. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Stephan Swiderski, Michael Parting, Jürgen Giesl, Carsten Fuhs, Peter Schneider-Kamp |
Termination Analysis by Dependency Pairs and Inductive Theorem Proving. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Feifei Ma, Sheng Liu, Jian Zhang 0001 |
Volume Computation for Boolean Combination of Linear Arithmetic Constraints. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Koen Claessen, Ann Lillieström |
Automated Inference of Finite Unsatisfiability. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda 0001, Patrick Wischnewski |
SPASS Version 3.5. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Matthias Horbach, Christoph Weidenbach |
Decidability Results for Saturation-Based Model Building. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | André Platzer, Jan-David Quesel, Philipp Rümmer |
Real World Verification. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
hybrid systems, software verification, decision procedures, Real-closed fields |
| 1 | Thomas Bouton, Diego Caminha Barbosa De Oliveira, David Déharbe, Pascal Fontaine |
veriT: An Open, Trustable and Efficient SMT-Solver. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Martin C. Rinard |
Integrated Reasoning and Proof Choice Point Selection in the Jahob System - Mechanisms for Program Survival. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani |
Interpolant Generation for UTVPI. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Roberto Sebastiani, Michele Vescovi |
Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Michel Ludwig, Ullrich Hustadt |
Fair Derivations in Monodic Temporal Reasoning. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Linh Anh Nguyen, Andrzej Szalas |
A Tableau Calculus for Regular Grammar Logics with Converse. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Konstantin Korovin |
Instantiation-Based Automated Reasoning: From Theory to Practice. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Stephan Falke 0001, Deepak Kapur |
A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Geoff Sutcliffe, Christoph Benzmüller, Chad E. Brown, Frank Theiss |
Progress in the Development of Automated Theorem Proving for Higher-Order Logic. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Renate A. Schmidt (eds.) |
Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Martin Korp, Aart Middeldorp |
Beyond Dependency Graphs. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Baumgartner 0001, Uwe Waldmann |
Superposition and Model Evolution Combined. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Viorica Sofronie-Stokkermans |
Locality Results for Certain Extensions of Theories with Bridging Functions. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Rajeev Goré, Florian Widmann |
An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Laura Kovács, Andrei Voronkov |
Interpolation and Symbol Elimination. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Stefan Ciobaca, Stéphanie Delaune, Steve Kremer |
Computing Knowledge in Security Protocols under Convergent Equational Theories. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Éric Grégoire, Bertrand Mazure, Cédric Piette |
Does This Set of Clauses Overlap with at Least One MUS? |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Lan Zhang 0001, Ullrich Hustadt, Clare Dixon |
A Refined Resolution Calculus for CTL. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Sean McLaughlin, Frank Pfenning |
Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Carsten Ihlemann, Viorica Sofronie-Stokkermans |
System Description: H-PILoT. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
local theory extensions, hierarchical reasoning |
| 1 | Bernard Boigelot, Julien Brusten, Jérôme Leroux |
A Generalization of Semenov's Theorem to Automata over Real Numbers. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Hicham Bensaid, Ricardo Caferra, Nicolas Peltier |
Dei: A Theorem Prover for Terms with Integer Exponents. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Cristina Borralleras, Salvador Lucas, Rafael Navarro-Marset, Enric Rodríguez-Carbonell, Albert Rubio |
Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
polynomial constraints, SAT modulo theories, program analysis, termination, Constraint solving |
| 1 | Maria Paola Bonacina, Christopher Lynch, Leonardo Mendonça de Moura |
On Deciding Satisfiability by DPLL(G+T) and Unsound Theorem Proving. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Guillem Godoy, Sophie Tison |
On the Normalization and Unique Normalization Properties of Term Rewrite Systems. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Bernhard Beckert, Martin Giese, Reiner Hähnle, Vladimir Klebanov, Philipp Rümmer, Steffen Schlager, Peter H. Schmitt |
The KeY system 1.0 (Deduction Component). |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Björn Pelzer, Christoph Wernhard |
System Description: E-KRHyper. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Roger Antonsen, Arild Waaler |
A Labelled System for IPL with Variable Splitting. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Höfner, Georg Struth |
Automated Reasoning in Kleene Algebra. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")
data released under the ODC-BY 1.0 license