11 Result(s)
within
Alexander J. Summers
English
Mathematical Logic and Formal Languages
-
Chapter and Conference Paper
A Formal Model to Prove Instantiation Termination for E-matching-Based Axiomatisations
SMT-based program analysis and verification often involve reasoning about program features that have been specified using quantifiers; incorporating quantifiers into SMT-based reasoning is, however, known to b...
-
Chapter and Conference Paper
Formally Validating a Practical Verification Condition Generator
A program verifier produces reliable results only if both the logic used to justify the program’s correctness is sound, and the implementation of the program verifier is itself correct. Whereas it is common to fo...
-
Chapter and Conference Paper
The Axiom Profiler: Understanding and Debugging SMT Quantifier Instantiations
SMT solvers typically reason about universal quantifiers via E-matching: syntactic matching patterns for each quantifier prescribe shapes of ground terms whose presence in the SMT run will trigger quantifier i...
-
Chapter and Conference Paper
Permission Inference for Array Programs
Information about the memory locations accessed by a program is, for instance, required for program parallelisation and program verification. Existing inference techniques for this information provide only par...
-
Chapter and Conference Paper
Automatic Verification of Iterated Separating Conjunctions Using Symbolic Execution
In permission logics such as separation logic, the iterated separating conjunction is a quantifier denoting access permission to an unbounded set of heap locations. In contrast to recursive predicates, iterate...
-
Chapter and Conference Paper
Viper: A Verification Infrastructure for Permission-Based Reasoning
The automation of verification techniques based on first-order logic specifications has benefitted greatly from verification infrastructures such as Boogie and Why. These offer an intermediate language that ca...
-
Chapter and Conference Paper
An Automatic Encoding from VeriFast Predicates into Implicit Dynamic Frames
VeriFast is a symbolic-execution-based verifier, based on separation logic specifications. Chalice is a verifier based on verification condition generation, which employs specifications in implicit dynamic fra...
-
Chapter and Conference Paper
Verification Condition Generation for Permission Logics with Abstract Predicates and Abstraction Functions
Abstract predicates are the primary abstraction mechanism for program logics based on access permissions, such as separation logic and implicit dynamic frames. In addition to abstract predicates, it is useful ...
-
Chapter and Conference Paper
A Formal Semantics for Isorecursive and Equirecursive State Abstractions
Methodologies for static program verification and analysis often support recursive predicates in specifications, in order to reason about recursive data structures. Intuitively, a predicate instance represents...
-
Chapter and Conference Paper
Abstract Read Permissions: Fractional Permissions without the Fractions
Fractional Permissions are a popular approach to reasoning about programs that use shared-memory concurrency, because they provide a way of proving data race freedom while permitting concurrent read access. Ho...
-
Chapter and Conference Paper
Approaches to Polymorphism in Classical Sequent Calculus
\(\mathcal X\) is a relatively new calculus, invented to give a Curry-Howard correspondence with Classical Implica...
