Journal: Journal of Automated Reasoning

Volume 60, Issue 4

385 -- 419Nicolas Matentzoglu, Bijan Parsia, Uli Sattler. OWL Reasoning: Subsumption Test Hardness and Modularity
421 -- 463Luis Aguirre, Narciso Martí-Oliet, Miguel Palomino, Isabel Pita. Sentence-Normalized Conditional Narrowing Modulo in Rewriting Logic and Maude
465 -- 501Salvador Lucas, Raúl Gutiérrez. Automatic Synthesis of Logical Models for Order-Sorted First-Order Theories
503 -- 526Eric Braude, Satbek Abdyldayev. Generalizing Morley's and Other Theorems with Automated Realization
527 -- 0John Slaney, Bruno Woltzenlogel Paleo. Erratum to: Conflict Resolution: A First-Order Resolution Calculus with Decision Literals and Conflict-Driven Clause Learning

Volume 60, Issue 3

255 -- 256Sandrine Blazy, Marsha Chechik. Selected Extended Papers of VSTTE 2016
257 -- 277Gang Tan, Greg Morrisett. Bidirectional Grammars for Machine-Code Decoding and Encoding
279 -- 298Kensuke Kojima, Akifumi Imanishi, Atsushi Igarashi. Automated Verification of Functional Correctness of Race-Free GPU Programs
299 -- 335Dirk Beyer 0001, Matthias Dangl, Philipp Wendler. A Unifying View on SMT-Based Software Verification
337 -- 363Moritz Kiefer, Vladimir Klebanov, Mattias Ulbrich. Relational Program Reasoning Using Compiler IR - Combining Static Verification and Dynamic Analysis
365 -- 383Martin Clochard, Léon Gondelman, Mário Pereira. The Matrix Reproved (Verification Pearl)

Volume 60, Issue 2

133 -- 156John Slaney, Bruno Woltzenlogel Paleo. Conflict Resolution: A First-Order Resolution Calculus with Decision Literals and Conflict-Driven Clause Learning
157 -- 176Zoltan A. Kocsis, Jerry Swan. Genetic Programming + Proof Search = Automatic Improvement
177 -- 220Laura Bozzelli, César Sánchez. Visibly Linear Temporal Logic
221 -- 236Filipe Casal, João Rasga. Many-Sorted Equivalence of Shiny and Strongly Polite Theories
237 -- 254Marco Maggesi. A Formalization of Metric Spaces in HOL Light

Volume 60, Issue 1

1 -- 2César A. Muñoz, Sanjai Rayadurgam, Oksana Tkachuk. Selected Extended Papers of NFM 2016: Preface
3 -- 21Julian Brunner, Peter Lammich. Formal Verification of an Executable LTL Model Checker with Partial Order Reduction
23 -- 42Shaobo He, Shuvendu K. Lahiri, Zvonimir Rakamaric. Verifying Relative Safety, Accuracy, and Termination for Program Approximations
43 -- 62Susmit Jha, Vasumathi Raman, Dorsa Sadigh, Sanjit A. Seshia. Safe Autonomy Under Perception Uncertainty Using Chance-Constrained Temporal Logic
63 -- 84Josh 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
85 -- 105Muhammad Usama Sardar, Nida Afaq, Osman Hasan, Khaza Anuarul Hoque. Towards Probabilistic Formal Analysis of SATS-Simultaneously Moving Aircraft (SATS-SMA)
107 -- 131Yi-Chin Wu, Vasumathi Raman, Blake C. Rawlings, Stéphane Lafortune, Sanjit A. Seshia. Synthesis of Obfuscation Policies to Ensure Privacy and Utility