| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Yannick Chevalier, Michaël Rusinowitch |
Decidability of Equivalence of Symbolic Derivations.  |
J. Autom. Reasoning  |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniele Zucchelli, Enrica Nicolini |
A Decidability Result for the Model Checking of Infinite-State Systems. |
J. Autom. Reasoning |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Predrag Janicic, Julien Narboux, Pedro Quaresma |
The Area Method - A Recapitulation. |
J. Autom. Reasoning |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael Codish, Jürgen Giesl, Peter Schneider-Kamp, René Thiemann |
SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs. |
J. Autom. Reasoning |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Steve Kremer, Antoine Mercier 0002, Ralf Treinen |
Reducing Equational Theories for the Decision of Static Equivalence. |
J. Autom. Reasoning |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Véronique Cortier, Stéphanie Delaune |
Decidability and Combination Results for Two Notions of Knowledge in Security Protocols. |
J. Autom. Reasoning |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Amy P. Felty, Alberto Momigliano |
Hybrid - A Definitional Two-Level Approach to Reasoning with Higher-Order Abstract Syntax. |
J. Autom. Reasoning |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Jan Otop |
E-unification with Constants vs. General E-unification. |
J. Autom. Reasoning |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Alexander Krauss, Tobias Nipkow |
Proof Pearl: Regular Expression Equivalence and Relation Algebra. |
J. Autom. Reasoning |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Freek Wiedijk |
"Handbook of Practical Logic and Automated Reasoning, " by John R. Harrison, Cambridge University Press, 2009. |
J. Autom. Reasoning |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Cristina Borralleras, Salvador Lucas, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio |
SAT Modulo Linear Arithmetic for Solving Polynomial Constraints. |
J. Autom. Reasoning |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Freek Verbeek, Julien Schmaltz |
Proof Pearl: A Formal Proof of Dally and Seitz' Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks. |
J. Autom. Reasoning |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Mnacho Echenim, Nicolas Peltier |
An Instantiation Scheme for Satisfiability Modulo Theories. |
J. Autom. Reasoning |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Stefan Ciobâca, Stéphanie Delaune, Steve Kremer |
Computing Knowledge in Security Protocols Under Convergent Equational Theories. |
J. Autom. Reasoning |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Siva Anantharaman, Hai Lin 0005, Christopher Lynch, Paliath Narendran, Michaël Rusinowitch |
Unification Modulo Homomorphic Encryption. |
J. Autom. Reasoning |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Belaid Benhamou, Lionel Paris, Pierre Siegel |
Dealing with Satisfiability and n-ary CSPs in a Logical Framework. |
J. Autom. Reasoning |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Joshua D. Guttman |
State and Progress in Strand Spaces: Proving Fair Exchange. |
J. Autom. Reasoning |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Hubert Comon-Lundh, Catherine Meadows |
Special Issue on Security and Rewriting Foreword. |
J. Autom. Reasoning |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Liang Chang, Zhongzhi Shi, Tianlong Gu, Lingzhong Zhao |
A Family of Dynamic Description Logics for Representing and Reasoning About Actions. |
J. Autom. Reasoning |
2012 |
DBLP DOI BibTeX RDF |
|
| 1 | Julian Backes, Chad E. Brown |
Analytic Tableaux for Higher-Order Logic with Choice. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Jasmin Christian Blanchette, Alexander Krauss |
Monotonicity Inference for Higher-Order Formulas. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Ole J. Mengshoel, Dan Roth, David C. Wilkins |
Portfolios in Stochastic Local Search: Efficiently Computing Most Probable Explanations in Bayesian Networks. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Carlos Areces, Daniel Gorín |
Resolution with Order and Selection for Hybrid Logics. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Koen Claessen, Ann Lillieström |
Automated Inference of Finite Unsatisfiability. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla |
Closed-Form Upper Bounds in Static Cost Analysis. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Javier Larrosa, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell |
A Framework for Certified Boolean Branch-and-Bound Optimization. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Lujo Bauer, Sandro Etalle, Jerry den Hartog, Luca Viganò |
Preface of Special Issue on "Computer Security: Foundations and Automated Reasoning". |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Moa Johansson, Lucas Dixon, Alan Bundy |
Conjecture Synthesis for Inductive Theories. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Amine Chaieb |
Formal Power Series. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Ralf Küsters, Tomasz Truderung |
Reducing Protocol Analysis with XOR to the XOR-Free Case in the Horn Theory Based Approach. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael J. C. Gordon, Matt Kaufmann, Sandip Ray |
The Right Tools for the Job: Correctness of Cone of Influence Reduction Proved Using ACL2 and HOL4. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Francisco-Jesús Martín-Mateos, José-Luis Ruiz-Reina, José-Antonio Alonso, María-José Hidalgo |
Proof Pearl: a Formal Proof of Higman's Lemma in ACL2. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Antonio Hernando, Eugenio Roanes-Lozano, Luis M. Laita |
A Polynomial Model for Logics with a Prime Power Number of Truth Values. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Nao Hirokawa, Aart Middeldorp |
Decreasing Diagrams and Relative Termination. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Gianni Ciolli, Graziano Gentili, Marco Maggesi |
A Certified Proof of the Cartan Fixed Point Theorems. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | John Thangarajah, Lin Padgham |
Computationally Effective Reasoning About Goal Interactions. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Baumgartner, Uwe Waldmann |
A Combined Superposition and Model Evolution Calculus. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Renate A. Schmidt, Brigitte Pientka |
Preface: Special Issue of Selected Extended Papers of CADE-22. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Véronique Cortier, Steve Kremer, Bogdan Warinschi |
A Survey of Symbolic Methods in Computational Analysis of Cryptographic Systems. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Maria Paola Bonacina, Christopher Lynch, Leonardo Mendonça de Moura |
On Deciding Satisfiability by Theorem Proving with Speculative Inferences. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Despoina Magka, Yevgeny Kazakov, Ian Horrocks |
Tractable Extensions of the Description Logic ${\mathcal{EL}}$ with Numerical Datatypes. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Jürgen Giesl, Reiner Hähnle |
Preface: Special Issue of Selected Extended Papers of IJCAR 2010. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Judicaël Courant, Marion Daubignard, Cristian Ene, Pascal Lafourcade, Yassine Lakhnech |
Automated Proofs for Asymmetric Encryption. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Hans de Nivelle |
Classical Logic with Partial Functions. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Louise A. Dennis, Ian Green, Alan Smaill |
The Use of Embeddings to Provide a Clean Separation of Term and Annotation for Higher Order Rippling. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Szymon Klarman, Ulle Endriss, Stefan Schlobach |
ABox Abduction in the Description Logic ALC. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Carsten Fuhs, Jürgen Giesl, Michael Parting, Peter Schneider-Kamp, Stephan Swiderski |
Proving Termination by Dependency Pairs and Inductive Theorem Proving. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Angelo Brillout, Daniel Kroening, Philipp Rümmer, Thomas Wahl |
An Interpolating Sequent Calculus for Quantifier-Free Presburger Arithmetic. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Wihem Arsac, Giampaolo Bella, Xavier Chantry, Luca Compagna |
Multi-Attacker Protocol Validation. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Max I. Kanovich, Paul Rowe, Andre Scedrov |
Collaborative Planning with Confidentiality. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Joana Martinho, António Ravara |
Encoding Cryptographic Primitives in a Calculus with Polyadic Synchronisation. |
J. Autom. Reasoning |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Ferruccio Guidi |
Procedural Representation of CIC Proof Terms. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Alessandro Armando, Peter Baumgartner, Gilles Dowek |
Preface. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Vivek Nigam, Dale Miller |
A Framework for Proof Systems. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Predrag Janicic |
Geometry Constructions Language. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Marius Bozga, Radu Iosif, Swann Perarnau |
Quantitative Separation Logic and Programs with Lists. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Knot Pipatsrisawat, Adnan Darwiche |
On Modern Clause-Learning Satisfiability Solvers. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Olivier Hermant |
Resolution is Cut-Free. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Dominik Dietrich, Ewaryst Schulz |
Crystal: Integrating Structured Queries into a Tactic Language. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Frédéric Pichon, Thierry Denoeux |
The Unnormalized Dempster's Rule of Combination: A New Justification from the Least Commitment Principle and Some Extensions. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Damiano Angeletti, Enrico Giunchiglia, Massimo Narizzano, Alessandra Puddu, Salvatore Sabina |
Using Bounded Model Checking for Coverage Analysis of Safety-Critical Software in an Industrial Setting. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Mauro Ferrari, Camillo Fiorentini, Guido Fiorino |
BCDL\boldsymbol {\cal BC\!D\!L}: Basic Constructive Description Logic. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Sascha Böhme, Michal Moskal, Wolfram Schulte, Burkhart Wolff |
HOL-Boogie - An Interactive Prover-Backend for the Verifying C Compiler. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Tobias Nipkow |
Linear Quantifier Elimination. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Bernhard Beckert, Reiner Hähnle |
Tests and Proofs - Preface of the Special Issue. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Delphine Longuet, Marc Aiguier, Pascale Le Gall |
Proof-Guided Test Selection from First-Order Specifications with Equality. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Bernardo Cuenca Grau, Christian Halaschek-Wiener, Yevgeny Kazakov, Boontawee Suntisrivaraporn |
Incremental Classification of Description Logics Ontologies. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Franz Baader, Rafael Peñaloza |
Automata-Based Axiom Pinpointing. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Jacques Carette, Makarius Wenzel, Freek Wiedijk |
Preface. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | James Cheney |
Equivariant Unification. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Lydie du Bousquet, Yves Ledru, Olivier Maury, Catherine Oriat, Jean-Louis Lanet |
Reusing a JML Specification Dedicated to Verification for Testing, and Vice-Versa: Case Studies. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Perry R. James, Patrice Chalin |
Faster and More Complete Extended Static Checking for the Java Modeling Language. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Zheng Ye, Shang-Ching Chou, Xiao-Shan Gao |
Visually Dynamic Presentation of Proofs in Plane Geometry - Part 1. Basic Features and the Manual Input Method. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Claudio Sacerdoti Coen |
Declarative Representation of Proof Terms. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Andriy Dunets, Gerhard Schellhorn, Wolfgang Reif |
Automated Flaw Detection in Algebraic Specifications. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Zheng Ye, Shang-Ching Chou, Xiao-Shan Gao |
Visually Dynamic Presentation of Proofs in Plane Geometry - Part 2. Automated Generation of Visually Dynamic Presentations with the Full-Angle Method and the Deductive Database Method. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Behzad Akbarpour, Lawrence C. Paulson |
MetiTarski: An Automatic Theorem Prover for Real-Valued Special Functions. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Miguel A. Palacios-Alonso, Carlos A. Brizuela, Luis Enrique Sucar |
Evolutionary Learning of Dynamic Naive Bayesian Classifiers. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael Mendler, Stephan Scheele |
Towards Constructive DL for Abstraction and Refinement. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | André Luiz Galdino, Mauricio Ayala-Rincón |
A Formalization of the Knuth-Bendix(-Huet) Critical Pair Theorem. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Gabriele Kern-Isberner, Manuela Ritterskamp |
Preference Fusion for Default Reasoning Beyond System Z. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Ruzica Piskac, Leonardo Mendonça de Moura, Nikolaj Bjørner |
Deciding Effectively Propositional Logic Using DPLL and Substitution Sets. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Andrea Calvagna, Angelo Gargantini |
A Formal Logic Approach to Constrained Combinatorial Testing. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Alexander Krauss |
Partial and Nested Recursive Function Definitions in Higher-order Logic. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Salem Benferhat, Safa Yahi, Habiba Drias |
A New Default Theories Compilation for MSP-Entailment. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Yang Xiang, Kevin Grant |
Preface: Special Issue on Uncertain Reasoning. |
J. Autom. Reasoning |
2010 |
DBLP DOI BibTeX RDF |
|
| 1 | Jean-François Dufourd |
An Intuitionistic Proof of a Discrete Form of the Jordan Curve Theorem Formalized in Coq with Combinatorial Hypermaps. |
J. Autom. Reasoning |
2009 |
DBLP DOI BibTeX RDF |
Computer-aided proofs, Coq system, Combinatorial hypermaps, Discrete Jordan Curve Theorem, Formal specifications, Computational topology, Planar subdivisions |
| 1 | Eyad Alkassar, Mark A. Hillebrand, Dirk Leinenbach, Norbert Schirmer, Artem Starostin, Alexandra Tsyban |
Balancing the Load. |
J. Autom. Reasoning |
2009 |
DBLP DOI BibTeX RDF |
Pervasive formal verification, Software verification, Systems verification |
| 1 | Marko Samer, Stefan Szeider |
Backdoor Sets of Quantified Boolean Formulas. |
J. Autom. Reasoning |
2009 |
DBLP DOI BibTeX RDF |
Backdoor sets, Variable dependencies, Parameterized complexity, Quantified Boolean formulas |
| 1 | K. Subramani |
Optimal Length Resolution Refutations of Difference Constraint Systems. |
J. Autom. Reasoning |
2009 |
DBLP DOI BibTeX RDF |
Difference constraint systems, Resolution refutation, Optimal length, Minimum unsatisfiable subset, Fourier-Motzkin elimination |
| 1 | María-del-Mar Gallardo, Pedro Merino, David Sanán |
Model Checking Dynamic Memory Allocation in Operating Systems. |
J. Autom. Reasoning |
2009 |
DBLP DOI BibTeX RDF |
Model checking, Operating systems, Dynamic memory allocation |
| 1 | John Harrison |
Formalizing an Analytic Proof of the Prime Number Theorem. |
J. Autom. Reasoning |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Raul Monroy, Alan Bundy, Ian Green |
On Process Equivalence = Equation Solving in CCS. |
J. Autom. Reasoning |
2009 |
DBLP DOI BibTeX RDF |
Unique fixpoint induction, Equational verification Calculus of communicating systems |
| 1 | Xinyu Feng, Zhong Shao, Yu Guo, Yuan Dong |
Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads. |
J. Autom. Reasoning |
2009 |
DBLP DOI BibTeX RDF |
Operating system verification, Hardware interrupts, Preemptive threads, Thread libraries, Modularity, Separation logic, Synchronization primitives |
| 1 | Syrine Tlili, Mourad Debbabi |
Interprocedural and Flow-Sensitive Type Analysis for Memory and Type Safety of C Code. |
J. Autom. Reasoning |
2009 |
DBLP DOI BibTeX RDF |
Type and effect analysis, C language, Type safety, Memory safety |
| 1 | Hendrik Tews, Marcus Völp, Tjark Weber |
Formal Memory Models for the Verification of Low-Level Operating-System Code. |
J. Autom. Reasoning |
2009 |
DBLP DOI BibTeX RDF |
Micro-hypervisor, Memory-mapped devices, Formal verification, Virtual memory, Operating-system kernel |
| 1 | Gerwin Klein, Ralf Huuck, Bastian Schlich |
Operating System Verification. |
J. Autom. Reasoning |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Xavier Leroy |
A Formally Verified Compiler Back-end. |
J. Autom. Reasoning |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Richard J. Boulton, Joe Hurd, Konrad Slind |
Computer Assisted Reasoning. |
J. Autom. Reasoning |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Giorgio Dalzotto, Tomás Recio |
On Protocols for the Automated Discovery of Theorems in Elementary Geometry. |
J. Autom. Reasoning |
2009 |
DBLP DOI BibTeX RDF |
Automatic theorem discovery, Elementary geometry, Computational algebraic geometry, Automatic theorem proving |
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")