317 citations · 355 across the 6 of their papers we have counts for
7 papers
Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Extended Version)
Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun +3
The introduction of separation logic has led to the development of symbolic execution techniques and tools that are (functionally) compositional with function specifications that c…
A Hybrid Approach to Semi-automated Rust Verification
Sacha-Élie Ayoun, Xavier Denis, Petar Maksimović +1
We propose a hybrid approach to end-to-end Rust verification where the proof effort is split into powerful automated verification of safe Rust and targeted semi-automated verificat…
Exact Separation Logic (Extended Version)
Petar Maksimović, Caroline Cronjäger, Andreas Lööw +2
Over-approximating (OX) program logics, such as separation logic (SL), are used for verifying properties of heap-manipulating programs: all terminating behaviour is characterised,…
: a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads
Furio Honsell, Luigi Liquori, Petar Maksimovic +1
We extend the constructive dependent type theory of the Logical Framework with monadic, dependent type constructors indexed with predicates over judgements, called Lo…
Gluing together Proof Environments: Canonical extensions of LF Type Theories featuring Locks
Furio Honsell, Luigi Liquori, Petar Maksimović +1
We present two extensions of the LF Constructive Type Theory featuring monadic locks. A lock is a monadic type construct that captures the effect of an external call to an oracle.…
Identifying boosted new physics with non-isolated leptons
Christopher Brust, Petar Maksimovic, Alice Sady +3
We demonstrate the utility of leptons which fail standard isolation criteria in searches for new physics at the LHC. Such leptons can arise in any event containing a highly boosted…
Jet Substructure at the Tevatron and LHC: New results, new tools, new benchmarks
A. Altheimer, S. Arora, L. Asquith +68
In this report we review recent theoretical progress and the latest experimental results in jet substructure from the Tevatron and the LHC. We review the status of and outlook for…