11 Result(s)
within
Alexander J. Summers
English
Software Engineering/Programming and Operating Systems
-
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
The Prusti Project: Formal Verification for Rust
Rust is a modern systems programming language designed to offer both performance and static safety. A key distinguishing feature is a strong type system, which enforces by default that memory is either shared ...
-
Chapter and Conference Paper
Sound Automation of Magic Wands
The magic wand \(\mathbin {-\!\!*}\) - ...
-
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...
-
Article
Automating deductive verification for weak-memory programs (extended version)
Writing correct programs for weak-memory models such as the C11 memory model is challenging because of the weak consistency guarantees these models provide. The first program logics for the verification of suc...
-
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
Automating Deductive Verification for Weak-Memory Programs
Writing correct programs for weak memory models such as the C11 memory model is challenging because of the weak consistency guarantees these models provide. The first program logics for the verification of suc...
-
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
Considerate Reasoning and the Composite Design Pattern
We propose Considerate Reasoning, a novel specification and verification technique based on object invariants. This technique supports succinct specifications of implementations which follow the pattern of breaki...
-
Chapter and Conference Paper
Universe Types for Topology and Encapsulation
The Universe Type System is an ownership type system for object-oriented programming languages that hierarchically structures the object store; it is used to reason modularly about programs.
-
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...
