97 citations · 156 across the 13 of their papers we have counts for
Showing 2015Show all
2 papers · 1 filter
cs.LO2015★ 6 cited
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)…
cs.LO2015★ 12 cited
The computability path ordering
Frédéric Blanqui, Jean-Pierre Jouannaud, Albert Rubio
This paper aims at carrying out termination proofs for simply typed higher-order calculi automatically by using ordering comparisons. To this end, we introduce the computability pa…