Verification, Model Checking, and Abstract Interpretation

7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings

E. Allen Emerson, Kedar S. Namjoshi (Herausgeber)

Buch | Softcover

XI, 443 Seiten

2005 | 2006
Springer Berlin (Verlag)
978-3-540-31139-3 (ISBN)

Artikel merken

lt;p>The 27 revised full papers presented here, together with one invited paper were carefully reviewed and selected from 58 submissions. The papers feature current research from the communities of verification, model checking, and abstract interpretation, facilitating interaction, cross-fertilization, and advancement of hybrid methods.

Closure Operators for ROBDDs.- A CLP Method for Compositional and Intermittent Predicate Abstraction.- Combining Shape Analyses by Intersecting Abstractions.- A Complete Abstract Interpretation Framework for Coverability Properties of WSTS.- Complexity Results on Branching-Time Pushdown Model Checking.- A Compositional Logic for Control Flow.- Detecting Non-cyclicity by Abstract Compilation into Boolean Functions.- Efficient Strongly Relational Polyhedral Analysis.- Environment Abstraction for Parameterized Verification.- Error Control for Probabilistic Model Checking.- Field Constraint Analysis.- A Framework for Certified Program Analysis and Its Applications to Mobile-Code Safety.- Improved Algorithm Complexities for Linear Temporal Logic Model Checking of Pushdown Systems.- A Logic and Decision Procedure for Predicate Abstraction of Heap-Manipulating Programs.- Monitoring Off-the-Shelf Components.- Parallel External Directed Model Checking with Linear I/O.- Piecewise FIFO Channels Are Analyzable.- Ranking Abstraction of Recursive Programs.- Relative Safety.- Resource Usage Analysis for the ?-Calculus.- Semantic Hierarchy Refactoring by Abstract Interpretation.- Strong Preservation of Temporal Fixpoint-Based Operators by Abstract Interpretation.- Symbolic Methods to Enhance the Precision of Numerical Abstract Domains.- Synthesis of Reactive(1) Designs.- Systematic Construction of Abstractions for Model-Checking.- Totally Clairvoyant Scheduling with Relative Timing Constraints.- Verification of Well-Formed Communicating Recursive State Machines.- What's Decidable About Arrays?.

Erscheint lt. Verlag	19.12.2005
Reihe/Serie	Lecture Notes in Computer Science
Reihe/Serie	Theoretical Computer Science and General Issues
Zusatzinfo	XI, 443 p.
Verlagsort	Berlin
Sprache	englisch
Maße	155 x 235 mm
Gewicht	640 g
Themenwelt	Mathematik / Informatik ► Informatik ► Software Entwicklung
Themenwelt	Informatik ► Theorie / Studium ► Compilerbau
Schlagworte	Abstract Interpretation • Abstraction • algorithms • Complexity • Design • Factor • formal methods • Formal Verification • Model Checking • program analysis • program invariants • programming • programming calculi • Program Semantics • Program specification • program validation • Program verification • Reactive Systems • Refactoring • Refinement • structured analysis • Temporal Logics • verification
ISBN-10	3-540-31139-4 / 3540311394
ISBN-13	978-3-540-31139-3 / 9783540311393
Zustand	Neuware