| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 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 | Feifei Ma, Sheng Liu, Jian Zhang 0001 |
Volume Computation for Boolean Combination of Linear Arithmetic Constraints. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Konstantin Korovin |
Instantiation-Based Automated Reasoning: From Theory to Practice. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Michel Ludwig, Ullrich Hustadt |
Fair Derivations in Monodic Temporal Reasoning. |
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 | Shuvendu K. Lahiri, Shaz Qadeer |
Complexity and Algorithms for Monomial and Clausal Predicate Abstraction. |
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 | Alessandro Cimatti, Alberto Griggio, Roberto Sebastiani |
Interpolant Generation for UTVPI. |
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 | Hicham Bensaid, Ricardo Caferra, Nicolas Peltier |
Dei: A Theorem Prover for Terms with Integer Exponents. |
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 | Viorica Sofronie-Stokkermans |
Locality Results for Certain Extensions of Theories with Bridging Functions. |
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 | 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 | Thomas Bouton, Diego Caminha B. de Oliveira, David Déharbe, Pascal Fontaine |
veriT: An Open, Trustable and Efficient SMT-Solver. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Stefan Ciobâca, Stéphanie Delaune, Steve Kremer |
Computing Knowledge in Security Protocols under Convergent Equational Theories. |
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 | 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 | Roberto Sebastiani, Michele Vescovi |
Axiom Pinpointing in Lightweight Description Logics via Horn-SAT Encoding and Conflict Analysis. |
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 | Peter Baumgartner, Uwe Waldmann |
Superposition and Model Evolution Combined. |
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 | Stephan Falke, Deepak Kapur |
A Term Rewriting Approach to the Automated Termination Analysis of Imperative Programs. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Christoph Weidenbach, Dilyana Dimova, Arnaud Fietzke, Rohit Kumar, Martin Suda, Patrick Wischnewski |
SPASS Version 3.5. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Laura Kovács, Andrei Voronkov |
Interpolation and Symbol Elimination. |
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 | Alex Roederer, Yury Puzis, Geoff Sutcliffe |
Divvy: An ATP Meta-system Based on Axiom Relevance Ordering. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Mark E. Stickel |
Building Theorem Provers. |
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 | Enrica Nicolini, Christophe Ringeissen, Michaël Rusinowitch |
Combinable Extensions of Abelian Groups. |
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 | Linh Anh Nguyen, Andrzej Szalas |
A Tableau Calculus for Regular Grammar Logics with Converse. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Koen Claessen, Ann Lillieström |
Automated Inference of Finite Unsatisfiability. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Lan Zhang, Ullrich Hustadt, Clare Dixon |
A Refined Resolution Calculus for CTL. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Martin Korp, Aart Middeldorp |
Beyond Dependency Graphs. |
CADE |
2009 |
DBLP DOI BibTeX RDF |
|
| 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 | Guodong Li, Konrad Slind |
Compilation as Rewriting in Higher Order Logic. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Frank Pfenning (eds.) |
Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings |
CADE |
2007 |
DBLP BibTeX RDF |
|
| 1 | Oleg Mürk, Daniel Larsson, Reiner Hähnle |
KeY-C: A Tool for Verification of C Programs. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Tal Lev-Ami, Christoph Weidenbach, Thomas W. Reps, Mooly Sagiv |
Labelled Clauses. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Carsten Lutz, Frank Wolter |
Conservative Extensions in the Lightweight Description Logic EL. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Christoph Weidenbach, Renate A. Schmidt, Thomas Hillenbrand, Rostislav Rusev, Dalibor Topic |
System Description: SpassVersion 3.0. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Christopher Lynch, Duc-Khanh Tran |
Automatic Decidability and Combinability Revisited. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Leonardo Mendonça de Moura, Nikolaj Bjørner |
Efficient E-Matching for SMT Solvers. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Björn Pelzer, Christoph Wernhard |
System Description: E-KRHyper. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Christian Urban, Stefan Berghofer, Michael Norrish |
Barendregt's Variable Convention in Rule Inductions. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Konstantin Verchinine, Alexander V. Lyaletski, Andrey Paskevich |
System for Automated Deduction (SAD): A Tool for Proof Verification. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Viktor Kuncak, Martin C. Rinard |
Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Boris Motik, Rob Shearer, Ian Horrocks |
Optimized Reasoning in Description Logics Using Hypertableaux. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Juan Antonio Navarro Pérez, Andrei Voronkov |
Encodings of Bounded LTL Model Checking in Effectively Propositional Logic. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Colin Stirling |
Games, Automata and Matching. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Geoff Sutcliffe, Yury Puzis |
SRASS - A Semantic Relevance Axiom Selection System. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Ashish Tiwari, Sumit Gulwani |
Logical Interpretation: Static Program Analysis Using Theorem Proving. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Gulay Ünel, David Toman |
An Incremental Technique for Automata-Based Decision Procedures. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Markus Aderhold |
Improvements in Formula Generalization. |
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 | David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu |
The Bedwyr System for Model Checking over Syntactic Expressions. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Baumgartner |
Logical Engineering with Instance-Based Methods. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Baumgartner, Ulrich Furbach, Björn Pelzer |
Hyper Tableaux with Equality. |
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 | Maria Paola Bonacina, Mnacho Echenim |
T-Decision by Decomposition. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Jean-François Couchot, Stéphane Lescuyer |
Handling Polymorphism in Automated Deduction. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Todd Deshane, Wenjin Hu, Patty Jablonski, Hai Lin, Christopher Lynch, Ralph Eric McGregor |
Encoding First Order Proofs in SAT. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Stephan Falke, Deepak Kapur |
Dependency Pairs for Rewriting with Non-free Constructors. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Yeting Ge, Clark Barrett, Cesare Tinelli |
Solving Quantified Verification Conditions Using Satisfiability Modulo Theories. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli |
Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Jürgen Giesl, René Thiemann, Stephan Swiderski, Peter Schneider-Kamp |
Proving Termination by Bounded Increase. |
CADE |
2007 |
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 | John Harrison |
Automating Elementary Number-Theoretic Proofs Using Gröbner Bases. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Osman Hasan, Sofiène Tahar |
Formalization of Continuous Probability Distributions. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Samuli Heilala, Brigitte Pientka |
Bidirectional Decision Procedures for the Intuitionistic Propositional Modal Logic IS4. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Höfner, Georg Struth |
Automated Reasoning in Kleene Algebra. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Adam Koprowski, Aart Middeldorp |
Predictive Labeling with Dependency Pairs Using SAT. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Alexander Krauss |
Certified Size-Change Termination. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | K. Rustan M. Leino |
Designing Verification Conditions for Software. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
| 1 | Robert Nieuwenhuis (eds.) |
Automated Deduction - CADE-20, 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005, Proceedings |
CADE |
2005 |
DBLP BibTeX RDF |
|
| 1 | Peter Baumgartner, Cesare Tinelli |
The Model Evolution Calculus with Equality. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Sean Bechhofer, Ian Horrocks, Daniele Turi |
The OWL Instance Store: System Description. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Serge Autexier |
The CoRe Calculus. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Marco Benedetti |
sKizzo: A Suite to Evaluate and Certify QBFs. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Franz Baader, Silvio Ghilardi |
Connecting Many-Sorted Theories. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Marco Bozzano, Roberto Bruttomesso, Alessandro Cimatti, Tommi A. Junttila, Peter van Rossum, Stephan Schulz, Roberto Sebastiani |
The MathSAT 3 System. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Evelyne Contejean, Pierre Corbineau |
Reflecting Proofs in First-Order Logic with Equality. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Chad E. Brown |
Reasoning in Extensional Type Theory with Equality. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Randal E. Bryant, Sanjit A. Seshia |
Decision Procedures Customized for Formal Verification. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Claudio Castellini, Alan Smaill |
Proof Planning for First-Order Temporal Logic. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Dowek |
What Do We Know When We Know That a Theory Is Consistent?. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Guillaume Dufay, Amy P. Felty, Stan Matwin |
Privacy-Sensitive Information Flow with JML. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Kaustuv Chaudhuri, Frank Pfenning |
A Focusing Inverse Method Theorem Prover for First-Order Linear Logic. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Christian G. Fermüller, Reinhard Pichler |
Model Representation via Contexts and Implicit Generalizations. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
Model computation, clause evaluation, model representation |
| 1 | Guillem Godoy, Ashish Tiwari |
Termination of Rewrite Systems with Shallow Right-Linear, Collapsing, and Right-Ground Rules. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Ullrich Hustadt, Boris Konev, Renate A. Schmidt |
Deciding Monodic Fragments by Temporal Resolution. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Boris Konev, Frank Wolter, Michael Zakharyaschev |
Temporal Logics over Transitive States. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Viktor Kuncak, Huu Hai Nguyen, Martin C. Rinard |
An Algorithm for Deciding BAPA: Boolean Algebra with Presburger Arithmetic. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Tal Lev-Ami, Neil Immerman, Thomas W. Reps, Shmuel Sagiv, Siddharth Srivastava, Greta Yorsh |
Simulating Reachability Using First-Order Logic with Applications to Verification of Linked Data Structures. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Jordi Levy, Joachim Niehren, Mateu Villaret |
Well-Nested Context Unification. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Sean McLaughlin, John Harrison |
A Proof-Producing Decision Procedure for Real Arithmetic. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Andreas Meier, Erica Melis |
System Description: Multi A Multi-strategy Proof Planner. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
| 1 | Mizuhito Ogawa, Eiichi Horita, Satoshi Ono |
Proving Properties of Incremental Merkle Trees. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
temporal authentication, theorem prover, Merkle tree |
| 1 | Brigitte Pientka |
Tabling for Higher-Order Logic Programming. |
CADE |
2005 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")