Journal: Journal of Automated Reasoning

Abbreviation

J. autom. reason.

Publisher

Springer

Journal Volumes

ISSN

0168-7433
1573-0670

Description

Filters

2003 - 200952010 - 20209
Reset filters

Search Results

Publications 1 - 10 of 14
  • Bytecode Verification by Model Checking
    Item type: Journal Article
    Basin, David; Friedrich, Stefan; Gawkowski, Marek (2003)
    Journal of Automated Reasoning
  • Completeness of a bytecode verifier and a certifying Java-to-JVM compiler
    Item type: Journal Article
    Stärk, Robert F.; Schmid, Joachim (2003)
    Journal of Automated Reasoning
  • Formalizing Network Flow Algorithms: A Refinement Approach in Isabelle/HOL
    Item type: Journal Article
    Lammich, Peter; Sefidgar, S. Reza (2019)
    Journal of Automated Reasoning
    We present a formalization of classical algorithms for computing the maximum flow in a network: the Edmonds–Karp algorithm and the push–relabel algorithm. We prove correctness and time complexity of these algorithms. Our formal proof closely follows a standard textbook proof, and is accessible even without being an expert in Isabelle/HOL—the interactive theorem prover used for the formalization. Using stepwise refinement techniques, we instantiate the generic Ford–Fulkerson algorithm to Edmonds–Karp algorithm, and the generic push–relabel algorithm of Goldberg and Tarjan to both the relabel-to-front and the FIFO push–relabel algorithm. Further refinement then yields verified efficient implementations of the algorithms, which compare well to unverified reference implementations.
  • An Extensible Encoding of Object-oriented Data Models in HOL
    Item type: Journal Article
    Brucker, Achim D.; Wolff, Burkhart (2008)
    Journal of Automated Reasoning
    We present an extensible encoding of object-oriented data models into higher-order logic (hol). Our encoding is supported by a datatype package that leverages the use of the shallow embedding technique to object-oriented specification and programming languages. The package incrementally compiles an object-oriented data model, i. e., a class model, to a theory containing object-universes, constructors, accessor functions, coercions (casts) between static types (and providing a foundation for the notion of dynamic types), characteristic sets, and co-inductive class invariants. The package is conservative, i. e., all properties are derived entirely from constant definitions, including the constraints over object structures. As an application, we use the package for an object-oriented core-language called imp++, for which we formally prove the correctness of a Hoare logic with respect to a denotational semantics.
  • Natural Projection as Partial Model Checking
    Item type: Journal Article
    Costa, Gabriele; Galletta, Letterio; Degano, Pierpaolo; et al. (2020)
    Journal of Automated Reasoning
    Verifying the correctness of a system as a whole requires establishing that it satisfies a global specification. When it does not, it would be helpful to determine which modules are incorrect. As a consequence, specification decomposition is a relevant problem from both a theoretical and practical point of view. Until now, specification decomposition has been independently addressed by the control theory and verification communities through natural projection and partial model checking, respectively. We prove that natural projection reduces to partial model checking and, when cast in a common setting, the two are equivalent. Apart from their foundational interest, our results build a bridge whereby the control theory community can reuse algorithms and results developed by the verification community. Furthermore, we extend the notions of natural projection and partial model checking from finite-state to symbolic transition systems and we show that the equivalence still holds. Symbolic transition systems are more expressive than traditional finite-state transition systems, as they can model large systems, whose behavior depends on the data handled, and not only on the control flow. Finally, we present an algorithm for the partial model checking of both kinds of systems that can be used as an alternative to natural projection.
  • A matrix characterization for multiplicative exponential linear logic
    Item type: Journal Article
    Kreitz, Christoph; Mantel, Heiko (2004)
    Journal of Automated Reasoning
  • Mechanising a Type-Safe Model of Multithreaded Java with a Verified Compiler
    Item type: Journal Article
    Lochbihler, Andreas (2018)
    Journal of Automated Reasoning
    This article presents JinjaThreads, a unified, type-safe model of multithreaded Java source code and bytecode formalised in the proof assistant Isabelle/HOL. The semantics strictly separates sequential aspects from multithreading features like locks, forks and joins, interrupts, and the wait-notify mechanism. This separation yields an interleaving framework and a notion of deadlocks that are independent of the language, and makes the type safety proofs modular. JinjaThreads’s non-optimising compiler translates source code into bytecode. Its correctness proof guarantees that the generated bytecode exhibits exactly the same observable behaviours as the source code, even for infinite executions and under the Java memory model. The semantics and the compiler are executable. JinjaThreads builds on and reuses the Java formalisations Jinja, Bali, 𝜇�Java, and Javaℓ𝑖�𝑔�ℎ𝑡� by Nipkow’s group. Being the result of more than fifteen years of studying Java in Isabelle/HOL, it constitutes a large and long-lasting case study. It shows that fairly standard formalisation techniques scale well and highlights the challenges, benefits, and drawbacks of formalisation reuse.
  • Formalizing Bachmair and Ganzinger’s Ordered Resolution Prover
    Item type: Journal Article
    Schlichtkrull, Anders; Blanchette, Jasmin; Traytel, Dmitriy; et al. (2020)
    Journal of Automated Reasoning
    We present an Isabelle/HOL formalization of the first half of Bachmair and Ganzinger's chapter on resolution theorem proving, culminating with a refutationally complete first-order prover based on ordered resolution with literal selection. We developed general infrastructure and methodology that can form the basis of completeness proofs for related calculi, including superposition. Our work clarifies fine points in the chapter, emphasizing the value of formal proofs in the field of automated reasoning. (© 2020 Springer).
  • Abstract Interpretation as Automated Deduction
    Item type: Journal Article
    D'Silva, Vijay; Urban, Caterina (2017)
    Journal of Automated Reasoning
  • Automated reasoning for security protocol analysis
    Item type: Other Journal Item
    Armando, Alessandro; Basin, David; Cuellar, Jorge; et al. (2006)
    Journal of Automated Reasoning
Publications 1 - 10 of 14