149 citations · 1.2k across the 55 of their papers we have counts for
13 papers · 1 filter
Model-Based Testing of an Intermediate Verifier Using Executable Operational Semantics
Lidia Losavio, Marco Paganoni, Carlo A. Furia
Lightweight validation technique, such as those based on random testing, are sometimes practical alternatives to full formal verification -- providing valuable benefits, such as fi…
VerifyThis 2019: A Program Verification Competition (Extended Report)
Claire Dross, Carlo A. Furia, Marieke Huisman +2
VerifyThis is a series of program verification competitions that emphasize the human aspect: participants tackle the verification of detailed behavioral properties -- something tha…
Why Just Boogie? Translating Between Intermediate Verification Languages
Michael Ameri, Carlo A. Furia
The verification systems Boogie and Why3 use their respective intermediate languages to generate verification conditions from high-level programs. Since the two systems support dif…
AutoProof: Auto-active Functional Verification of Object-oriented Programs
Julian Tschannen, Carlo A. Furia, Martin Nordio +1
Auto-active verifiers provide a level of automation intermediate between fully automatic and interactive: users supply code with annotations as input while benefiting from a high l…
Rotation of Sequences: Algorithms and Proofs
Carlo A. Furia
Sequence rotation consists of a circular shift of the sequence's elements by a given number of positions. We present the four classic algorithms to rotate a sequence; the loop inva…
Bounded Variability of Metric Temporal Logic
Carlo A. Furia, Paola Spoletini
Previous work has shown that reasoning with real-time temporal logics is often simpler when restricted to models with bounded variability---where no more than v events may occur ev…