Abstract is missing.
- Formal Methods for PrivacyMichael Carl Tschantz, Jeannette M. Wing. 1-15 [doi]
- What Can Formal Methods Bring to Systems Biology?Nicola Bonzanni, K. Anton Feenstra, Wan Fokkink, Elzbieta Krepska. 16-22 [doi]
- Guess and Verify - Back to the FutureColin O Halloran. 23-32 [doi]
- Verification, Testing and StatisticsSriram K. Rajamani. 33-40 [doi]
- Security, Probability and Nearly Fair Coins in the Cryptographers CaféAnnabelle McIver, Larissa Meinicke, Carroll Morgan. 41-71 [doi]
- Recursive Abstractions for Parameterized SystemsJoxan Jaffar, Andrew E. Santosa. 72-88 [doi]
- Abstract Model Checking without Computing the AbstractionStefano Tonetta. 89-105 [doi]
- Three-Valued Spotlight AbstractionsJonas Schrieb, Heike Wehrheim, Daniel Wonisch. 106-122 [doi]
- Fair Model Checking with Process Counter AbstractionJun Sun 0001, Yang Liu 0003, Abhik Roychoudhury, Shanshan Liu, Jin Song Dong. 123-139 [doi]
- Systematic Development of Trustworthy Component SystemsRodrigo Ramos, Augusto Sampaio, Alexandre Mota. 140-156 [doi]
- Partial Order Reductions Using Compositional Confluence DetectionFrédéric Lang, Radu Mateescu. 157-172 [doi]
- A Formal Method for Developing Provably Correct Fault-Tolerant Systems Using Partial Refinement and CompositionRalph D. Jeffords, Constance L. Heitmeyer, Myla Archer, Elizabeth I. Leonard. 173-189 [doi]
- Abstract Specification of the UBIFS File System for Flash MemoryAndreas Schierl, Gerhard Schellhorn, Dominik Haneberg, Wolfgang Reif. 190-206 [doi]
- Inferring Mealy MachinesMuzammil Shahbaz, Roland Groz. 207-222 [doi]
- Formal Management of CAD/CAM ProcessesMichael Kohlhase, Johannes Lemburg, Lutz Schröder, Ewaryst Schulz. 223-238 [doi]
- Translating Safe Petri Nets to Statecharts in a Structure-Preserving WayRik Eshuis. 239-255 [doi]
- Symbolic Predictive Analysis for Concurrent ProgramsChao Wang, Sudipta Kundu, Malay K. Ganai, Aarti Gupta. 256-272 [doi]
- On the Difficulties of Concurrent-System Design, Illustrated with a 2×2 Switch Case StudyEdgar G. Daylight, Sandeep K. Shukla. 273-288 [doi]
- ::::Sums and Lovers: :::: Case Studies in Security, Compositionality and RefinementAnnabelle McIver, Carroll C. Morgan. 289-304 [doi]
- Iterative Refinement of Reverse-Engineered Models by Model-Based TestingNeil Walkinshaw, John Derrick, Qiang Guo. 305-320 [doi]
- Model Checking Linearizability via RefinementYang Liu 0003, Wei Chen, Yanhong A. Liu, Jun Sun 0001. 321-337 [doi]
- It s Doomed; We Can Prove ItJochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, Thomas Wies. 338-353 [doi]
- Carbon Credits for Resource-Bounded Computations Using Amortised AnalysisSteffen Jost, Hans-Wolfgang Loidl, Kevin Hammond, Norman Scaife, Martin Hofmann. 354-369 [doi]
- Field-Sensitive Value Analysis by Field-Insensitive AnalysisElvira Albert, Puri Arenas, Samir Genaim, Germán Puebla. 370-386 [doi]
- Making Temporal Logic Calculational: A Tool for Unification and DiscoveryRaymond Boute. 387-402 [doi]
- A Tableau for CTLMark Reynolds. 403-418 [doi]
- Certifiable Specification and Verification of C ProgramsChristoph Lüth, Dennis Walter. 419-434 [doi]
- Formal Reasoning about Expectation Properties for Continuous Random VariablesOsman Hasan, Naeem Abbasi, Behzad Akbarpour, Sofiène Tahar, Reza Akbarpour. 435-450 [doi]
- The Denotational Semantics of slotted-CircusPawel Gancarski, Andrew Butterfield. 451-466 [doi]
- Unifying Probability with NondeterminismYifeng Chen, Jeff W. Sanders. 467-482 [doi]
- Towards an Operational Semantics for AlloyTheophilos Giannakopoulos, Daniel J. Dougherty, Kathi Fisler, Shriram Krishnamurthi. 483-498 [doi]
- A Robust Semantics Hides Fewer ErrorsSteve Reeves, David Streader. 499-515 [doi]
- Analysis of a Clock Synchronization Protocol for Wireless Sensor NetworksFaranak Heidarian, Julien Schmaltz, Frits W. Vaandrager. 516-531 [doi]
- Formal Verification of Avionics Software ProductsJean Souyris, Virginie Wiels, David Delmas, Hervé Delseny. 532-546 [doi]
- Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case StudyAndré Platzer, Edmund M. Clarke. 547-562 [doi]
- Connecting UML and VDM++ with Open Tool SupportKenneth Lausdahl, Hans Kristian Agerlund Lintrup, Peter Gorm Larsen. 563-578 [doi]
- Language and Tool Support for Class and State Machine Refinement in UML-BMar Yah Said, Michael J. Butler, Colin F. Snook. 579-595 [doi]
- Dynamic Classes: Modular Asynchronous Evolution of Distributed Concurrent ObjectsEinar Broch Johnsen, Marcel Kyas, Ingrid Chieh Yu. 596-611 [doi]
- Abstract Object Creation in Dynamic LogicWolfgang Ahrendt, Frank S. de Boer, Immo Grabe. 612-627 [doi]
- Reasoning about Memory LayoutsHolger Gast. 628-643 [doi]
- A Smooth Combination of Linear and Herbrand Equalities for Polynomial Time Must-Alias AnalysisHelmut Seidl, Vesal Vojdani, Varmo Vene. 644-659 [doi]
- On the Complexity of Synthesizing Relaxed and Graceful Bounded-Time 2-Phase RecoveryBorzoo Bonakdarpour, Sandeep S. Kulkarni. 660-675 [doi]
- Verifying Real-Time Systems against Scenario-Based RequirementsKim Guldstrand Larsen, Shuhao Li, Brian Nielsen, Saulius Pusinskas. 676-691 [doi]
- Formal Specification of a Cardiac Pacing SystemArtur Oliveira Gomes, Marcel Vinicius Medeiros Oliveira. 692-707 [doi]
- Automated Property Verification for Large Scale B ModelsMichael Leuschel, Jérôme Falampin, Fabian Fritz, Daniel Plagge. 708-723 [doi]
- Reduced Execution Semantics of MPI: From Theory to PracticeSarvani S. Vakkalanka, Anh Vo, Ganesh Gopalakrishnan, Robert M. Kirby. 724-740 [doi]
- A Metric Encoding for Bounded Model CheckingMatteo Pradella, Angelo Morzenti, Pierluigi San Pietro. 741-756 [doi]
- An Incremental Approach to Scope-Bounded Checking Using a Lightweight Formal MethodDanhua Shao, Sarfraz Khurshid, Dewayne E. Perry. 757-772 [doi]
- Verifying Information Flow Control over Unbounded ProcessesWilliam R. Harris, Nicholas Kidd, Sagar Chaki, Somesh Jha, Thomas W. Reps. 773-789 [doi]
- Specification and Verification of Web Applications in Rewriting LogicMaría Alpuente, Demis Ballis, Daniel Romero. 790-805 [doi]
- Verifying the Microsoft Hyper-V Hypervisor with VCCDirk Leinenbach, Thomas Santen. 806-809 [doi]
- Industrial Practice in Formal Methods: A ReviewJuan Bicarregui, John S. Fitzgerald, Peter Gorm Larsen, J. C. P. Woodcock. 810-813 [doi]
- Model-Based GUI Testing Using Uppaal at Novo NordiskUlrik H. Hjort, Jacob Illum Rasmussen, Kim Guldstrand Larsen, Michael A. Petersen, Arne Skou. 814-818 [doi]