10 Result(s)
within
Alexander J. Summers
English
Programming Languages, Compilers, Interpreters
-
Chapter and Conference Paper
Local Reasoning for Global Graph Properties
Separation logics are widely used for verifying programs that manipulate complex heap-based data structures. These logics build on so-called separation algebras, which allow expressing properties of heap regions ...
-
Chapter and Conference Paper
Actor Services
We present actor services: a novel program logic for defining and verifying response and functional properties of programs which communicate via asynchronous messaging. Actor services can specify how parts of ...
-
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
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...
-
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...
