publication . Other literature type . Article . Conference object . 2018

Modularity for Decidability of Deductive Verification with Applications to Distributed Systems

Mooly Sagiv; Marcelo Taube; Sharon Shoham; James R. Wilcox; Doug Woos; Kenneth L. McMillan; Oded Padon; Giuliano Losa;
Open Access English
  • Published: 16 Apr 2018
  • Publisher: Zenodo
This is the artifact of the paper. Its a compressed virtual machine that can be imported by VirtualBox. Abstract of the paper: Proof automation can substantially increase productivity in formal verification of complex systems. However, unpredictablility of automated provers in handling quantified formulas presents a major hurdle to usability of these tools. We propose to solve this problem not by improving the provers, but by using a modular proof methodology that allows us to produce \emph{decidable} verification conditions. Decidability greatly improves predictability of proof automation, resulting in a more practical verification approach. We apply this metho...
free text keywords: Software, Computer Graphics and Computer-Aided Design, Modularity, Decidability, Formal verification, Modular design, business.industry, business, Usability, Programming language, computer.software_genre, computer, Paxos, Computer science, Automation, Complex system
Funded by
Supervised Verification of Infinite-State Systems
  • Funder: European Commission (EC)
  • Project Code: 759102
  • Funding stream: H2020 | ERC | ERC-STG
Download fromView all 8 versions
Other literature type . 2018
Provider: Datacite
Article . 2018
Provider: ZENODO
Other literature type . 2018
Provider: Datacite
Other literature type . 2018
Provider: Datacite
Any information missing or wrong?Report an Issue