432 citations · 2.3k across the 29 of their papers we have counts for
4 papers · 1 filter
Inferring Lower Runtime Bounds for Integer Programs
Florian Frohn, Matthias Naaf, Marc Brockschmidt +1
We present a technique to infer lower bounds on the worst-case runtime complexity of integer programs, where in contrast to earlier work, our approach is not restricted to tail-rec…
T2: Temporal Property Verification
Marc Brockschmidt, Byron Cook, Samin Ishtiaq +2
We present the open-source tool T2, the first public release from the TERMINATOR project. T2 has been extended over the past decade to support automatic temporal-logic proving tech…
Compositional Safety Verification with Max-SMT
Marc Brockschmidt, Daniel Larraz, Albert Oliveras +2
We present an automated compositional program verification technique for safety properties based on conditional inductive invariants. For a given program part (e.g., a single loop)…
CTL+FO Verification as Constraint Solving
Tewodros A. Beyene, Marc Brockschmidt, Andrey Rybalchenko
Expressing program correctness often requires relating program data throughout (different branches of) an execution. Such properties can be represented using CTL+FO, a logic that a…