Search
 
loader loading subjects...
cover
Verification and Synthesis of Reactive Programs
Amir Pnueli
298 - 340
NATO Security through Science Series - D: Information and Communication Security
Volume 9: Software System Reliability and Security
Abstract

In these notes we present a viable approach to the synthesis of reactive programs from a temporal specification of their desired behavior. When successful, this direct correct-by-construction approach to system development obviates the need for post-facto verification.

In spite of the established double exponential lower bound that applies to the general case, we show that many useful specifications fall into a class of temporal formulas, technically identified as the Reactivity(1) class, for which we present an n3 synthesis algorithm.

$35.00 / €27.50 / £22.00
Add PDF to cart