![](https://dblp.uni-trier.de./img/logo.320x120.png)
![search dblp search dblp](https://dblp.uni-trier.de./img/search.dark.16x16.png)
![search dblp](https://dblp.uni-trier.de./img/search.dark.16x16.png)
default search action
Journal of Automated Reasoning, Volume 60
Volume 60, Number 1, January 2018
- César A. Muñoz, Sanjai Rayadurgam, Oksana Tkachuk:
Selected Extended Papers of NFM 2016: Preface. 1-2 - Julian Brunner
, Peter Lammich
:
Formal Verification of an Executable LTL Model Checker with Partial Order Reduction. 3-21 - Shaobo He
, Shuvendu K. Lahiri, Zvonimir Rakamaric:
Verifying Relative Safety, Accuracy, and Termination for Program Approximations. 23-42 - Susmit Jha
, Vasumathi Raman, Dorsa Sadigh, Sanjit A. Seshia:
Safe Autonomy Under Perception Uncertainty Using Chance-Constrained Temporal Logic. 43-62 - Josh Newell
, Linna Pang, David Tremaine, Alan Wassyng, Mark Lawford:
Translation of IEC 61131-3 Function Block Diagrams to PVS for Formal Verification with Real-Time Nuclear Application. 63-84 - Muhammad Usama Sardar
, Nida Afaq, Osman Hasan
, Khaza Anuarul Hoque:
Towards Probabilistic Formal Analysis of SATS-Simultaneously Moving Aircraft (SATS-SMA). 85-105 - Yi-Chin Wu, Vasumathi Raman, Blake C. Rawlings
, Stéphane Lafortune
, Sanjit A. Seshia:
Synthesis of Obfuscation Policies to Ensure Privacy and Utility. 107-131
Volume 60, Number 2, February 2018
- John K. Slaney
, Bruno Woltzenlogel Paleo
:
Conflict Resolution: A First-Order Resolution Calculus with Decision Literals and Conflict-Driven Clause Learning. 133-156 - Zoltan A. Kocsis
, Jerry Swan
:
Genetic Programming + Proof Search = Automatic Improvement. 157-176 - Laura Bozzelli, César Sánchez
:
Visibly Linear Temporal Logic. 177-220 - Filipe Casal
, João Rasga
:
Many-Sorted Equivalence of Shiny and Strongly Polite Theories. 221-236 - Marco Maggesi
:
A Formalization of Metric Spaces in HOL Light. 237-254
Volume 60, Number 3, March 2018
- Sandrine Blazy
, Marsha Chechik:
Selected Extended Papers of VSTTE 2016. 255-256 - Gang Tan
, Greg Morrisett:
Bidirectional Grammars for Machine-Code Decoding and Encoding. 257-277 - Kensuke Kojima
, Akifumi Imanishi, Atsushi Igarashi
:
Automated Verification of Functional Correctness of Race-Free GPU Programs. 279-298 - Dirk Beyer
, Matthias Dangl
, Philipp Wendler
:
A Unifying View on SMT-Based Software Verification. 299-335 - Moritz Kiefer, Vladimir Klebanov, Mattias Ulbrich
:
Relational Program Reasoning Using Compiler IR - Combining Static Verification and Dynamic Analysis. 337-363 - Martin Clochard, Léon Gondelman, Mário Pereira
:
The Matrix Reproved (Verification Pearl). 365-383
Volume 60, Number 4, April 2018
- Nicolas Matentzoglu
, Bijan Parsia
, Uli Sattler
:
OWL Reasoning: Subsumption Test Hardness and Modularity. 385-419 - Luis Aguirre
, Narciso Martí-Oliet
, Miguel Palomino
, Isabel Pita
:
Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude. 421-463 - Salvador Lucas
, Raúl Gutiérrez
:
Automatic Synthesis of Logical Models for Order-Sorted First-Order Theories. 465-501 - Eric Braude
, Satbek Abdyldayev:
Generalizing Morley's and Other Theorems with Automated Realization. 503-526 - John K. Slaney
, Bruno Woltzenlogel Paleo
:
Erratum to: Conflict Resolution: A First-Order Resolution Calculus with Decision Literals and Conflict-Driven Clause Learning. 527
![](https://dblp.uni-trier.de./img/cog.dark.24x24.png)
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.