Last update: Sun Aug 5 02:03:07 MDT 2018
@Article{Bastani:2000:RP,
author = "Farokh B. Bastani",
title = "Relational programs",
journal = j-SIGSOFT,
volume = "25",
number = "1",
pages = "34--35",
month = jan,
year = "2000",
CODEN = "SFENDP",
DOI = "https://doi.org/10.1145/340855.340865",
ISSN = "0163-5948 (print), 1943-5843 (electronic)",
ISSN-L = "0163-5948",
bibdate = "Wed Aug 1 17:13:50 MDT 2018",
bibsource = "http://www.math.utah.edu/pub/tex/bib/sigsoft2000.bib",
abstract = "The objective of this research is to produce useful,
low-cost methods for developing correct concurrent
programs from formal specifications. In particular, we
address the design and verification of the
synchronization and communication portions of such
programs. Often, this portion can be implemented using
a fixed, finite amount of synchronization related data,
i.e., it is ``finite-state.'' Nevertheless, even when
each program component contains only one bit of
synchronization related data, the number of possible
global synchronization states for K components is about
$ 2^K $, in general. Because of this
``state-explosion'' phenomenon, the manual verification
of large concurrent programs typically requires
lengthy, and therefore error-prone, proofs. Using a
theorem prover increases reliability, but requires
extensive formal labor to axiomatize and solve
verification problems. Automatic verification methods
(such as reachability analysis and temporal logic model
checking) use state-space exploration to decide if a
program satisfies its specification, and are therefore
also subject to state-explosion. To date, proposed
techniques for ameliorating state-explosion either
require significant manual labor, or work well only
when the program is highly symmetric and regular (e.g.,
many functionally similar components connected in
similar ways). To overcome these drawbacks, we advocate
the synthesis of programs from specifications. This
approach performs the refinement from specifications to
programs automatically. Thus, the amount of formal
labor is reduced to writing a formal specification and
applying the appropriate synthesis step at each stage
of the derivation. While nontrivial, writing a formal
specification is necessary in any methodology that
guarantees correctness.",
acknowledgement = ack-nhfb,
fjournal = "ACM SIGSOFT Software Engineering Notes",
journal-URL = "https://dl.acm.org/citation.cfm?id=J728",
}