Abstract. We address the issue of efficiently automating assume-guarantee reasoning for simulation conformance between finite state systems and specifications. We focus on a non...
Sagar Chaki, Edmund M. Clarke, Nishant Sinha, Pras...
We present a complete method for synthesizing lexicographic linear ranking functions supported by inductive linear invariants for loops with linear guards and transitions. Proving ...
This paper presents a toolset for model checking x86 executables. The members of the toolset are CodeSurfer/x86, WPDS++, and the Path Inspector. CodeSurfer/x86 is used to extract a...
Gogul Balakrishnan, Thomas W. Reps, Nicholas Kidd,...