20 citations · 50 across the 12 of their papers we have counts for
Showing 2020 · cs.LOShow all
2 papers · 2 filters
cs.LO2020★ 1 cited
Cuvée: Blending SMT-LIB with Programs and Weakest Preconditions
Gidon Ernst
Cuvée is a program verification tool that reads SMT-LIB-like input files where terms may additionally contain weakest precondition operators over abstract programs. Cuvée translate…
cs.LO2020★ 1 cited
A Complete Approach to Loop Verification with Invariants and Summaries
Gidon Ernst
Invariants are the predominant approach to verify the correctness of loops. As an alternative, loop contracts, which make explicit the premise and conclusion of the underlying indu…