default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDFM 2009: Eindhoven, The Netherlands
- Ana Cavalcanti, Dennis Dams:
FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings. Lecture Notes in Computer Science 5850, Springer 2009, ISBN 978-3-642-05088-6
Invited Papers
- Michael Carl Tschantz, Jeannette M. Wing:
Formal Methods for Privacy. 1-15 - Nicola Bonzanni, K. Anton Feenstra
, Wan J. Fokkink, Elzbieta Krepska:
What Can Formal Methods Bring to Systems Biology? 16-22 - Colin O'Halloran:
Guess and Verify - Back to the Future. 23-32 - Sriram K. Rajamani:
Verification, Testing and Statistics. 33-40 - Annabelle McIver, Larissa Meinicke, Carroll Morgan:
Security, Probability and Nearly Fair Coins in the Cryptographers' Café. 41-71
Model Checking I
- Joxan Jaffar, Andrew E. Santosa:
Recursive Abstractions for Parameterized Systems. 72-88 - Stefano Tonetta:
Abstract Model Checking without Computing the Abstraction. 89-105 - Jonas Schrieb, Heike Wehrheim, Daniel Wonisch:
Three-Valued Spotlight Abstractions. 106-122 - Jun Sun, Yang Liu, Abhik Roychoudhury, Shanshan Liu, Jin Song Dong:
Fair Model Checking with Process Counter Abstraction. 123-139
Compositionality
- Rodrigo Ramos, Augusto Sampaio, Alexandre Mota:
Systematic Development of Trustworthy Component Systems. 140-156 - Frédéric Lang, Radu Mateescu:
Partial Order Reductions Using Compositional Confluence Detection. 157-172 - Ralph D. Jeffords, Constance L. Heitmeyer, Myla Archer, Elizabeth I. Leonard:
A Formal Method for Developing Provably Correct Fault-Tolerant Systems Using Partial Refinement and Composition. 173-189
Verification
- Andreas Schierl, Gerhard Schellhorn, Dominik Haneberg, Wolfgang Reif:
Abstract Specification of the UBIFS File System for Flash Memory. 190-206 - Muzammil Shahbaz, Roland Groz:
Inferring Mealy Machines. 207-222 - Michael Kohlhase, Johannes Lemburg, Lutz Schröder, Ewaryst Schulz:
Formal Management of CAD/CAM Processes. 223-238
Concurrency
- Rik Eshuis:
Translating Safe Petri Nets to Statecharts in a Structure-Preserving Way. 239-255 - Chao Wang, Sudipta Kundu, Malay K. Ganai, Aarti Gupta:
Symbolic Predictive Analysis for Concurrent Programs. 256-272 - Edgar G. Daylight, Sandeep K. Shukla:
On the Difficulties of Concurrent-System Design, Illustrated with a 2×2 Switch Case Study. 273-288
Refinement
- Annabelle McIver, Carroll C. Morgan:
Sums and Lovers: Case Studies in Security, Compositionality and Refinement. 289-304 - Neil Walkinshaw, John Derrick, Qiang Guo:
Iterative Refinement of Reverse-Engineered Models by Model-Based Testing. 305-320 - Yang Liu, Wei Chen, Yanhong A. Liu, Jun Sun:
Model Checking Linearizability via Refinement. 321-337
Static Analysis
- Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, Thomas Wies:
It's Doomed; We Can Prove It. 338-353 - Steffen Jost, Hans-Wolfgang Loidl, Kevin Hammond, Norman Scaife, Martin Hofmann:
"Carbon Credits" for Resource-Bounded Computations Using Amortised Analysis. 354-369 - Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla:
Field-Sensitive Value Analysis by Field-Insensitive Analysis. 370-386
Theorem Proving
- Raymond T. Boute:
Making Temporal Logic Calculational: A Tool for Unification and Discovery. 387-402 - Mark Reynolds:
A Tableau for CTL. 403-418 - Christoph Lüth, Dennis Walter:
Certifiable Specification and Verification of C Programs. 419-434 - Osman Hasan, Naeem Abbasi, Behzad Akbarpour, Sofiène Tahar, Reza Akbarpour:
Formal Reasoning about Expectation Properties for Continuous Random Variables. 435-450
Semantics
- Pawel Gancarski, Andrew Butterfield:
The Denotational Semantics of slotted-Circus. 451-466 - Yifeng Chen, Jeff W. Sanders:
Unifying Probability with Nondeterminism. 467-482 - Theophilos Giannakopoulos, Daniel J. Dougherty, Kathi Fisler, Shriram Krishnamurthi:
Towards an Operational Semantics for Alloy. 483-498 - Steve Reeves, David Streader:
A Robust Semantics Hides Fewer Errors. 499-515
Special Track: Industrial Applications I
- Faranak Heidarian, Julien Schmaltz, Frits W. Vaandrager:
Analysis of a Clock Synchronization Protocol for Wireless Sensor Networks. 516-531 - Jean Souyris, Virginie Wiels, David Delmas, Hervé Delseny:
Formal Verification of Avionics Software Products. 532-546 - André Platzer, Edmund M. Clarke:
Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study. 547-562
Object-Orientation
- Kenneth Lausdahl, Hans Kristian Agerlund Lintrup, Peter Gorm Larsen:
Connecting UML and VDM++ with Open Tool Support. 563-578 - Mar Yah Said, Michael J. Butler, Colin F. Snook:
Language and Tool Support for Class and State Machine Refinement in UML-B. 579-595 - Einar Broch Johnsen, Marcel Kyas, Ingrid Chieh Yu:
Dynamic Classes: Modular Asynchronous Evolution of Distributed Concurrent Objects. 596-611 - Wolfgang Ahrendt, Frank S. de Boer, Immo Grabe:
Abstract Object Creation in Dynamic Logic. 612-627
Pointers
- Holger Gast:
Reasoning about Memory Layouts. 628-643 - Helmut Seidl, Vesal Vojdani, Varmo Vene:
A Smooth Combination of Linear and Herbrand Equalities for Polynomial Time Must-Alias Analysis. 644-659
Real-Time
- Borzoo Bonakdarpour, Sandeep S. Kulkarni:
On the Complexity of Synthesizing Relaxed and Graceful Bounded-Time 2-Phase Recovery. 660-675 - Kim Guldstrand Larsen, Shuhao Li, Brian Nielsen, Saulius Pusinskas:
Verifying Real-Time Systems against Scenario-Based Requirements. 676-691
Special Track: Tools and Industrial Applications II
- Artur Oliveira Gomes, Marcel Vinícius Medeiros Oliveira:
Formal Specification of a Cardiac Pacing System. 692-707 - Michael Leuschel, Jérôme Falampin, Fabian Fritz, Daniel Plagge:
Automated Property Verification for Large Scale B Models. 708-723 - Sarvani S. Vakkalanka, Anh Vo, Ganesh Gopalakrishnan, Robert M. Kirby:
Reduced Execution Semantics of MPI: From Theory to Practice. 724-740
Model Checking II
- Matteo Pradella, Angelo Morzenti, Pierluigi San Pietro:
A Metric Encoding for Bounded Model Checking. 741-756 - Danhua Shao, Sarfraz Khurshid, Dewayne E. Perry:
An Incremental Approach to Scope-Bounded Checking Using a Lightweight Formal Method. 757-772 - William R. Harris, Nicholas Kidd, Sagar Chaki, Somesh Jha, Thomas W. Reps:
Verifying Information Flow Control over Unbounded Processes. 773-789 - María Alpuente, Demis Ballis, Daniel Romero:
Specification and Verification of Web Applications in Rewriting Logic. 790-805
Industry-Day Abstracts
- Dirk Leinenbach, Thomas Santen:
Verifying the Microsoft Hyper-V Hypervisor with VCC. 806-809 - Juan Bicarregui, John S. Fitzgerald, Peter Gorm Larsen, J. C. P. Woodcock:
Industrial Practice in Formal Methods: A Review. 810-813 - Ulrik H. Hjort, Jacob Illum Rasmussen, Kim Guldstrand Larsen, Michael A. Petersen, Arne Skou:
Model-Based GUI Testing Using Uppaal at Novo Nordisk. 814-818
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2025-10-31 00:54 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
