6 Result(s)
within
English
Artificial Intelligence
Alexander J. Summers
Conference Paper
-
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
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...
-
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
The Relationship between Separation Logic and Implicit Dynamic Frames
Separation logic is a concise method for specifying programs that manipulate dynamically allocated storage. Partially inspired by separation logic, Implicit Dynamic Frames has recently been proposed, aiming at...
