Thomas Pani
YOU?
Author Swipe
View article: Technical Report: Exploring Automatic Model-Checking of the Ethereum specification
Technical Report: Exploring Automatic Model-Checking of the Ethereum specification Open
We investigate automated model-checking of the Ethereum specification, focusing on the Accountable Safety property of the 3SF consensus protocol. We select 3SF due to its relevance and the unique challenges it poses for formal verification…
View article: Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification
Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification Open
Parameterized programs are composed of an arbitrary number of concurrent, infinite-state threads. Automated safety and liveness proofs of such parameterized software are hard; state-of-the-art methods for their formal verification rely on …
View article: Rely-guarantee bound analysis of parameterized concurrent shared-memory programs
Rely-guarantee bound analysis of parameterized concurrent shared-memory programs Open
We present a thread-modular proof method for complexity and resource bound analysis of concurrent, shared-memory programs. To this end, we lift Jones’ rely-guarantee reasoning to assumptions and commitments capable of expressing bounds. Th…
View article: Thread-modular Counter Abstraction for Parameterized Program Safety
Thread-modular Counter Abstraction for Parameterized Program Safety Open
Automated safety proofs of parameterized software are hard: State-of-the-art methods rely on intricate abstractions and complicated proof techniques that often impede automation. We replace this heavy machinery with a clean abstraction fra…
View article: Empirical software metrics for benchmarking of verification tools
Empirical software metrics for benchmarking of verification tools Open
We study empirical metrics for software source code, which can predict the performance of verification tools on specific types of software. Our metrics comprise variable usage patterns, loop patterns, as well as indicators of control-flow …
View article: Loop Patterns in C Programs
Loop Patterns in C Programs Open
In this work, we conduct a systematic study of loops in C programs. We describe static analyses capable of efficiently identifying definite iteration in C code. Our experiments show that over one third of loops in our benchmarks take this …