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

Modularity for Decidability of Deductive Verification with Applications to Distributed Systems

Name: Modularity for decidability of deductive verification with applications to distributed systems
Keywords: Software, Computer Graphics and Computer-Aided Design

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

Summary

Abstract

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...

doi: 10.5281/zenodo.2577103 , 10.5281/zenodo.1218853 , 10.5281/zenodo.1218852 ...

View all 5 identifiers

Subjects

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

Related Organizations