E-Book, Englisch, 443 Seiten, eBook
Emerson / Namjoshi Verification, Model Checking, and Abstract Interpretation
2006
ISBN: 978-3-540-31622-0
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark
7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings
E-Book, Englisch, 443 Seiten, eBook
Reihe: Theoretical Computer Science and General Issues
ISBN: 978-3-540-31622-0
Verlag: Springer
Format: PDF
Kopierschutz: 1 - PDF Watermark
Zielgruppe
Research
Autoren/Hrsg.
Weitere Infos & Material
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?.