Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
1 | Matteo Pradella, Angelo Morzenti, Pierluigi San Pietro |
A Metric Encoding for Bounded Model Checking. |
FM |
2009 |
DBLP DOI BibTeX RDF |
Bounded model checking, metric temporal logic |
1 | Steffen Jost, Hans-Wolfgang Loidl, Kevin Hammond, Norman Scaife, Martin Hofmann 0001 |
"Carbon Credits" for Resource-Bounded Computations Using Amortised Analysis. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Raymond T. Boute |
Making Temporal Logic Calculational: A Tool for Unification and Discovery. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | William R. Harris, Nicholas Kidd, Sagar Chaki, Somesh Jha, Thomas W. Reps |
Verifying Information Flow Control over Unbounded Processes. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Rik Eshuis |
Translating Safe Petri Nets to Statecharts in a Structure-Preserving Way. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Jonas Schrieb, Heike Wehrheim, Daniel Wonisch |
Three-Valued Spotlight Abstractions. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | 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. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Dirk Leinenbach, Thomas Santen |
Verifying the Microsoft Hyper-V Hypervisor with VCC. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Steve Reeves, David Streader |
A Robust Semantics Hides Fewer Errors. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Osman Hasan, Naeem Abbasi, Behzad Akbarpour, Sofiène Tahar, Reza Akbarpour |
Formal Reasoning about Expectation Properties for Continuous Random Variables. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Theophilos Giannakopoulos, Daniel J. Dougherty, Kathi Fisler, Shriram Krishnamurthi |
Towards an Operational Semantics for Alloy. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Juan Bicarregui, John S. Fitzgerald, Peter Gorm Larsen, J. C. P. Woodcock |
Industrial Practice in Formal Methods: A Review. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Einar Broch Johnsen, Marcel Kyas, Ingrid Chieh Yu |
Dynamic Classes: Modular Asynchronous Evolution of Distributed Concurrent Objects. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Faranak Heidarian, Julien Schmaltz, Frits W. Vaandrager |
Analysis of a Clock Synchronization Protocol for Wireless Sensor Networks. |
FM |
2009 |
DBLP DOI BibTeX RDF |
wireless sensor networks, model checking, theorem proving, timed automata, clock synchronization, industrial application |
1 | Pawel Gancarski, Andrew Butterfield |
The Denotational Semantics of slotted-Circus. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Jean Souyris, Virginie Wiels, David Delmas, Hervé Delseny |
Formal Verification of Avionics Software Products. |
FM |
2009 |
DBLP DOI BibTeX RDF |
avionics software, verification, formal verification, static analysis, Abstract Interpretation, safety, development process |
1 | Mark Reynolds 0001 |
A Tableau for CTL. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Annabelle McIver, Larissa Meinicke, Carroll Morgan |
Security, Probability and Nearly Fair Coins in the Cryptographers' Café. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Artur Oliveira Gomes, Marcel Vinícius Medeiros Oliveira |
Formal Specification of a Cardiac Pacing System. |
FM |
2009 |
DBLP DOI BibTeX RDF |
formal modelling, Z, industrial applications, pacemaker |
1 | Ana Cavalcanti 0001, Dennis Dams (eds.) |
FM 2009: Formal Methods, Second World Congress, Eindhoven, The Netherlands, November 2-6, 2009. Proceedings |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Christoph Lüth, Dennis Walter |
Certifiable Specification and Verification of C Programs. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Jun Sun 0001, Yang Liu 0003, Abhik Roychoudhury, Shanshan Liu, Jin Song Dong |
Fair Model Checking with Process Counter Abstraction. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | André Platzer, Edmund M. Clarke |
Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Jochen Hoenicke, K. Rustan M. Leino, Andreas Podelski, Martin Schäf, Thomas Wies |
It's Doomed; We Can Prove It. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Yifeng Chen, Jeff W. Sanders |
Unifying Probability with Nondeterminism. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Muzammil Shahbaz, Roland Groz |
Inferring Mealy Machines. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Colin O'Halloran |
Guess and Verify - Back to the Future. |
FM |
2009 |
DBLP DOI BibTeX RDF |
Models, Verification, Software, Automation, Cost, Proof, Simulink |
1 | Kenneth Lausdahl, Hans Kristian Agerlund Lintrup, Peter Gorm Larsen |
Connecting UML and VDM++ with Open Tool Support. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Nicola Bonzanni, K. Anton Feenstra, Wan J. Fokkink, Elzbieta Krepska |
What Can Formal Methods Bring to Systems Biology? |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Borzoo Bonakdarpour, Sandeep S. Kulkarni |
On the Complexity of Synthesizing Relaxed and Graceful Bounded-Time 2-Phase Recovery. |
FM |
2009 |
DBLP DOI BibTeX RDF |
Bounded-time recovery, Phased recovery, Fault-tolerance, Real-time, Program transformation, Program synthesis |
1 | Michael Carl Tschantz, Jeannette M. Wing |
Formal Methods for Privacy. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | María Alpuente, Demis Ballis, Daniel Romero 0001 |
Specification and Verification of Web Applications in Rewriting Logic. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Sriram K. Rajamani |
Verification, Testing and Statistics. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Andreas Schierl, Gerhard Schellhorn, Dominik Haneberg, Wolfgang Reif |
Abstract Specification of the UBIFS File System for Flash Memory. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Mar Yah Said, Michael J. Butler, Colin F. Snook |
Language and Tool Support for Class and State Machine Refinement in UML-B. |
FM |
2009 |
DBLP DOI BibTeX RDF |
UML, Formal specification, Refinement, Event-B, Visual modelling languages |
1 | Helmut Seidl, Vesal Vojdani, Varmo Vene |
A Smooth Combination of Linear and Herbrand Equalities for Polynomial Time Must-Alias Analysis. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla |
Field-Sensitive Value Analysis by Field-Insensitive Analysis. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Kim Guldstrand Larsen, Shuhao Li, Brian Nielsen, Saulius Pusinskas |
Verifying Real-Time Systems against Scenario-Based Requirements. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Neil Walkinshaw, John Derrick, Qiang Guo 0001 |
Iterative Refinement of Reverse-Engineered Models by Model-Based Testing. |
FM |
2009 |
DBLP DOI BibTeX RDF |
Reverse engineering, model-based testing, Erlang |
1 | Annabelle McIver, Carroll C. Morgan |
Sums and Lovers: Case Studies in Security, Compositionality and Refinement. |
FM |
2009 |
DBLP DOI BibTeX RDF |
Refinement of security, formalised secrecy, hierarchical security reasoning, compositional semantics |
1 | Joxan Jaffar, Andrew E. Santosa |
Recursive Abstractions for Parameterized Systems. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Stefano Tonetta |
Abstract Model Checking without Computing the Abstraction. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Michael Leuschel, Jérôme Falampin, Fabian Fritz, Daniel Plagge |
Automated Property Verification for Large Scale B Models. |
FM |
2009 |
DBLP DOI BibTeX RDF |
Model Checking, Tools, Constraint-Solving, Industrial Applications, B-Method |
1 | Ulrik H. Hjort, Jacob Illum Rasmussen, Kim Guldstrand Larsen, Michael A. Petersen, Arne Skou |
Model-Based GUI Testing Using Uppaal at Novo Nordisk. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Edgar G. Daylight, Sandeep K. Shukla |
On the Difficulties of Concurrent-System Design, Illustrated with a 2×2 Switch Case Study. |
FM |
2009 |
DBLP DOI BibTeX RDF |
adaptability, non-functional requirements, formal specification languages, local reasoning |
1 | Sarvani S. Vakkalanka, Anh Vo, Ganesh Gopalakrishnan, Robert M. Kirby |
Reduced Execution Semantics of MPI: From Theory to Practice. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Rodrigo Ramos, Augusto Sampaio, Alexandre Mota 0001 |
Systematic Development of Trustworthy Component Systems. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Frédéric Lang, Radu Mateescu 0001 |
Partial Order Reductions Using Compositional Confluence Detection. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Holger Gast |
Reasoning about Memory Layouts. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Chao Wang 0001, Sudipta Kundu, Malay K. Ganai, Aarti Gupta |
Symbolic Predictive Analysis for Concurrent Programs. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Wolfgang Ahrendt, Frank S. de Boer, Immo Grabe |
Abstract Object Creation in Dynamic Logic. |
FM |
2009 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Noll 0001, Stefan Rieger |
Verifying Dynamic Pointer-Manipulating Threads. |
FM |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Klaas Wijbrans, Franc Buve, Robin Rijkers, Wouter Geurts |
Software Engineering with Formal Methods: Experiences with the Development of a Storm Surge Barrier Control System. |
FM |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Michael Emmi, Dimitra Giannakopoulou, Corina S. Pasareanu |
Assume-Guarantee Verification for Interface Automata. |
FM |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Holger Grandy, Markus Bischof, Kurt Stenzel, Gerhard Schellhorn, Wolfgang Reif |
Verification of Mondex Electronic Purses with KIV: From a Security Protocol to Verified Code. |
FM |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Arvind, Nirav Dave, Michael Katelman |
Getting Formal Verification into Design Flow. |
FM |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Alexander Harhurin, Judith Hartmann |
Towards Consistent Specifications of Product Families. |
FM |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Emina Torlak, Felix Sheng-Ho Chang, Daniel Jackson 0001 |
Finding Minimal Unsatisfiable Cores of Declarative Specifications. |
FM |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Torben Amtoft, John Hatcliff, Edwin Rodríguez, Robby, Jonathan Hoag, David A. Greve |
Specification and Checking of Software Contracts for Conditional Information Flow. |
FM |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Eric Verhulst, Gjalt G. de Jong, Vitaliy Mezhuyev |
An Industrial Case: Pitfalls and Benefits of Applying Formal Methods to the Development of a Network-Centric RTOS. |
FM |
2008 |
DBLP DOI BibTeX RDF |
Network centric, Security, Formal Methods, Safety, Trustworthy, RTOS |
1 | Radu Mateescu 0001, Damien Thivolle |
A Model Checking Language for Concurrent Value-Passing Systems. |
FM |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Shmuel Katz |
Aspects and Formal Methods. |
FM |
2008 |
DBLP DOI BibTeX RDF |
model-checking, specification, interference, detection, Aspects |
1 | Engin Uzuncaova, Sarfraz Khurshid |
Constraint Prioritization for Efficient Analysis of Declarative Models. |
FM |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Johan Dovland, Einar Broch Johnsen, Olaf Owe, Martin Steffen |
Lazy Behavioral Subtyping. |
FM |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Thierry Lecomte |
Safe and Reliable Metro Platform Screen Doors Control/Command Systems. |
FM |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Boutheina Chetali, Quang Huy Nguyen 0002 |
Industrial Use of Formal Methods for a High-Level Security Evaluation. |
FM |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Joseph R. Kiniry, Daniel M. Zimmerman |
Secret Ninja Formal Methods. |
FM |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Jorge Cuéllar, T. S. E. Maibaum, Kaisa Sere (eds.) |
FM 2008: Formal Methods, 15th International Symposium on Formal Methods, Turku, Finland, May 26-30, 2008, Proceedings |
FM |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Scott Lintelman, Richard Robinson, Mingyan Li, Krishna Sampigethaya |
Formal Methods for Trustworthy Skies: Building Confidence in the Security of Aircraft Assets Distribution. |
FM |
2008 |
DBLP DOI BibTeX RDF |
Loadable Software Parts, Security, Formal Methods, Safety |
1 | Patrice Chalin, Frédéric Rioux |
JML Runtime Assertion Checking: Improved Error Reporting and Efficiency Using Strong Validity. |
FM |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Tom Ridge, Michael Norrish, Peter Sewell |
A Rigorous Approach to Networking: TCP, from Implementation to Protocol to Service. |
FM |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Tim McComb, Graeme Smith 0001 |
Introducing Objects through Refinement. |
FM |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Taro Kurita, Miki Chiba, Yasumasa Nakatsugawa |
Application of a Formal Specification Language in the Development of the "Mobile FeliCa" IC Chip Firmware for Embedding in Mobile Phone. |
FM |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Anna Zaks, Amir Pnueli |
CoVaC: Compiler Validation by Program Analysis of the Cross-Product. |
FM |
2008 |
DBLP DOI BibTeX RDF |
|
1 | David Kitchin, Evan Powell, Jayadev Misra |
Simulation, Orchestration and Logical Clocks. |
FM |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Thomas Gawlitza, Helmut Seidl |
Precise Interval Analysis vs. Parity Games. |
FM |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Borzoo Bonakdarpour, Sandeep S. Kulkarni |
Masking Faults While Providing Bounded-Time Phased Recovery. |
FM |
2008 |
DBLP DOI BibTeX RDF |
Bounded-time recovery, Phased recovery, Fault-tolerance, Real-time, Formal methods, Synthesis, Transformation |
1 | Arsenii Rudich, Ádám Darvas, Peter Müller 0001 |
Checking Well-Formedness of Pure-Method Specifications. |
FM |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Olivier Ponsini, Wendelin Serwe |
A Schedulerless Semantics of TLM Models Written in SystemC Via Translation into LOTOS. |
FM |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Irem Aktug, Mads Dam, Dilian Gurov |
Provably Correct Runtime Monitoring. |
FM |
2008 |
DBLP DOI BibTeX RDF |
|
1 | A. K. McIver, Carroll C. Morgan, Carlos Gonzalía |
Proofs and Refutations for Probabilistic Refinement. |
FM |
2008 |
DBLP DOI BibTeX RDF |
quantitative program logic, refinement, constraint solving, counterexamples, Probabilistic systems |
1 | Carlo A. Furia, Matteo Pradella, Matteo Rossi |
Automated Verification of Dense-Time MTL Specifications Via Discrete-Time Approximation. |
FM |
2008 |
DBLP DOI BibTeX RDF |
real-time, sampling, discretization, metric temporal logic, verification techniques, dense time |
1 | Hugo Daniel Macedo, Peter Gorm Larsen, John S. Fitzgerald |
Incremental Development of a Distributed Real-Time Model of a Cardiac Pacing System Using VDM. |
FM |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Dawson R. Engler |
Lessons in the Weird and Unexpected: Some Experiences from Checking Large Real Systems. |
FM |
2008 |
DBLP DOI BibTeX RDF |
|
1 | Jim Woodcock 0001 |
Verified Software Grand Challenge. |
FM |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Gerhard Schellhorn, Holger Grandy, Dominik Haneberg, Wolfgang Reif |
The Mondex Challenge: Machine Checked Proofs for an Electronic Purse. |
FM |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Amir Pnueli, Aleksandr Zaks |
PSL Model Checking and Run-Time Verification Via Testers. |
FM |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Jan Jürjens |
Model-Based Security Engineering for Real. |
FM |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Thomas A. Henzinger, Joseph Sifakis |
The Embedded Systems Design Challenge. |
FM |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Pamela Zave |
Compositional Binding in Network Domains. |
FM |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Michael Backes 0001, Birgit Pfitzmann, Michael Waidner |
Formal Methods and Cryptography. |
FM |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Jonathan Schmitt, Alwin Hoffmann, Michael Balser, Wolfgang Reif, Mar Marcos |
Interactive Verification of Medical Guidelines. |
FM |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Alcino Cunha, José Nuno Oliveira, Joost Visser 0001 |
Type-Safe Two-Level Data Transformation. |
FM |
2006 |
DBLP DOI BibTeX RDF |
|
1 | José Nuno Oliveira, César Jesus Rodrigues |
Pointfree Factorization of Operation Refinement. |
FM |
2006 |
DBLP DOI BibTeX RDF |
reusable theories, refinement, Theoretical foundations, calculation |
1 | D. Randolph Johnson |
Cost Effective Software Engineering for Security. |
FM |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Sandrine Blazy, Zaynah Dargaye, Xavier Leroy |
Formal Verification of a C Compiler Front-End. |
FM |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Alastair F. Donaldson, Alice Miller 0001 |
Exact and Approximate Strategies for Symmetry Reduction in Model Checking. |
FM |
2006 |
DBLP DOI BibTeX RDF |
Promela/Spin, computational group theory, model checking, symmetry, Gap |
1 | Viorel Preoteasa |
Mechanical Verification of Recursive Procedures Manipulating Pointers Using Separation Logic. |
FM |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Mass Soldal Lund, Ketil Stølen |
A Fully General Operational Semantics for UML 2.0 Sequence Diagrams with Potential and Mandatory Choice. |
FM |
2006 |
DBLP DOI BibTeX RDF |
|
1 | Marcel Verhoef, Peter Gorm Larsen, Jozef Hooman |
Modeling and Validating Distributed Embedded Real-Time Systems with VDM++. |
FM |
2006 |
DBLP DOI BibTeX RDF |
|