| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Cristian Gherghina, Cristina David, Shengchao Qin, Wei-Ngan Chin |
Structured Specifications for Better Verification of Heap-Manipulating Programs.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Peter Müller, Joseph N. Ruskiewicz |
Using Debuggers to Understand Failed Verification Attempts.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Elvira Albert, Samir Genaim, Miguel Gómez-Zamalloa, Einar Broch Johnsen, Rudolf Schlatte, Silvia Lizeth Tapia Tarifa |
Simulating Concurrent Behaviors with Worst-Case Cost Bounds.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Juan Manuel Crespo, César Kunz |
Relational Verification Using Product Programs.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Javier de Dios, Ricardo Peña |
Certification of Safe Polynomial Memory Bounds.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Dominique Méry, Mohamed Mosbah, Mohamed Tounsi |
Refinement-Based Verification of Local Synchronization Algorithms.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Sarah M. Loos, André Platzer, Ligia Nistor |
Adaptive Cruise Control: Hybrid, Distributed, and Now Formally Verified.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Werner Damm, Bernd Finkbeiner |
Does It Pay to Extend the Perimeter of a World Model?  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Jasmin Fisher, Nir Piterman, Moshe Y. Vardi |
The Only Way Is Up.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Steve Dunne |
Termination without \checkmark\checkmark in CSP.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | John Derrick, Gerhard Schellhorn, Heike Wehrheim |
Verifying Linearisability with Potential Linearisation Points.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Kristin Y. Rozier, Moshe Y. Vardi |
A Multi-encoding Approach for LTL Symbolic Satisfiability Checking.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | David Harel |
Some Thoughts on Behavioral Programming.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Borzoo Bonakdarpour, Samaneh Navabpour, Sebastian Fischmeister |
Sampling-Based Runtime Verification.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Ana Cavalcanti, Andy J. Wellings, Jim Woodcock |
The Safety-Critical Java Memory Model: A Formal Account.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Shao Jie Zhang, Jun Sun 0001, Jun Pang, Yang Liu 0003, Jin Song Dong |
On Combining State Space Reductions with Global Fairness Assumptions.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Anne Elisabeth Haxthausen, Andreas A. Kjær, Marie Le Bliguet |
Formal Development of a Tool for Automated Modelling and Verification of Relay Interlocking Systems.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Nuno Amálio, Christian Glodt, Pierre Kelsen |
Building VCL Models and Automatically Generating Z Specifications from Them.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Gabriel Ciobanu, Maciej Koutny |
Timed Migration and Interaction with Access Permissions.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Shengchao Qin, Chenguang Luo, Wei-Ngan Chin, Guanhua He |
Automatically Refining Partial Specifications for Program Verification.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Jonathan P. Bowen, Steve Reeves |
From a Community of Practice to a Body of Knowledge: A Case Study of the Formal Methods Community.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael Butler, Wolfram Schulte (eds.) |
FM 2011: Formal Methods - 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Aboubakr Achraf El Ghazi, Mana Taghdiri |
Relational Reasoning via SMT Solving.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Howard Barringer, Klaus Havelund |
TraceContract: A Scala DSL for Trace Analysis.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael J. Banks, Jeremy L. Jacob |
Specifying Confidentiality in Circus.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Zhenbang Chen, Zhiming Liu, Ji Wang |
Failure-Divergence Refinement of Compensating Communicating Processes.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Guodong Li |
Validated Compilation through Logic.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Daniel Dietsch, Bernd Westphal, Andreas Podelski |
System Verification through Program Verification.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Vladimir Klebanov, Peter Müller, Natarajan Shankar, Gary T. Leavens, Valentin Wüstholz, Eyad Alkassar, Rob Arthan, Derek Bronish, Rod Chapman, Ernie Cohen, Mark A. Hillebrand, Bart Jacobs, K. Rustan M. Leino, Rosemary Monahan, Frank Piessens, Nadia Polikarpova, Tom Ridge, Jan Smans, Stephan Tobies, Thomas Tuerk, Mattias Ulbrich, Benjamin Weiß |
The 1st Verified Software Competition: Experience Report.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Janos Sztipanovits |
Model Integration and Cyber Physical Systems: A Semantics Perspective.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Fabienne Boyer, Olivier Gruber, Gwen Salaün |
Specifying and Verifying the SYNERGY Reconfiguration Protocol with LOTOS NT and CADP.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna |
Formally Verifying Isolation and Availability in an Idealized Model of Virtualization.  |
FM  |
2011 |
DBLP DOI BibTeX RDF |
|
| 1 | Bart Jacobs, Jan Smans, Frank Piessens |
Verification of Unloadable Modules.  |
FM  |
2011 |
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 | Frédéric Lang, Radu Mateescu |
Partial Order Reductions Using Compositional Confluence Detection.  |
FM  |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Pawel Gancarski, Andrew Butterfield |
The Denotational Semantics of slotted-Circus.  |
FM  |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Jonas Schrieb, Heike Wehrheim, Daniel Wonisch |
Three-Valued Spotlight Abstractions.  |
FM  |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Artur Oliveira Gomes, Marcel Vinicius Medeiros Oliveira |
Formal Specification of a Cardiac Pacing System.  |
FM  |
2009 |
DBLP DOI BibTeX RDF |
formal modelling, Z, industrial applications, pacemaker |
| 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 | Dirk Leinenbach, Thomas Santen |
Verifying the Microsoft Hyper-V Hypervisor with VCC.  |
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 | Stefano Tonetta |
Abstract Model Checking without Computing the Abstraction.  |
FM  |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Steve Reeves, David Streader |
A Robust Semantics Hides Fewer Errors.  |
FM  |
2009 |
DBLP DOI BibTeX RDF |
|
| 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 | Yifeng Chen, Jeff W. Sanders |
Unifying Probability with Nondeterminism.  |
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 | Yang Liu 0003, Wei Chen 0013, Yanhong A. Liu, Jun Sun 0001 |
Model Checking Linearizability via Refinement.  |
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 | Rodrigo Ramos, Augusto Sampaio, Alexandre Mota |
Systematic Development of Trustworthy Component Systems.  |
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 | Mark Reynolds |
A Tableau for CTL.  |
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 | 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 | 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 | Nicola Bonzanni, K. Anton Feenstra, Wan Fokkink, Elzbieta Krepska |
What Can Formal Methods Bring to Systems Biology?  |
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 | Chao Wang, Sudipta Kundu, Malay K. Ganai, Aarti Gupta |
Symbolic Predictive Analysis for Concurrent Programs.  |
FM  |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Muzammil Shahbaz, Roland Groz |
Inferring Mealy Machines.  |
FM  |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Holger Gast |
Reasoning about Memory Layouts.  |
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 | Ana Cavalcanti, 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 | Elvira Albert, Puri Arenas, Samir Genaim, Germán Puebla |
Field-Sensitive Value Analysis by Field-Insensitive Analysis.  |
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 | 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 | Michael Carl Tschantz, Jeannette M. Wing |
Formal Methods for Privacy.  |
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 | Theophilos Giannakopoulos, Daniel J. Dougherty, Kathi Fisler, Shriram Krishnamurthi |
Towards an Operational Semantics for Alloy.  |
FM  |
2009 |
DBLP DOI BibTeX RDF |
|
| 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 | Neil Walkinshaw, John Derrick, Qiang Guo |
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, Larissa Meinicke, Carroll Morgan |
Security, Probability and Nearly Fair Coins in the Cryptographers' Café.  |
FM  |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Joxan Jaffar, Andrew E. Santosa |
Recursive Abstractions for Parameterized Systems.  |
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 | 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 | 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 | 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 |
"Carbon Credits" for Resource-Bounded Computations Using Amortised Analysis.  |
FM  |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Danhua Shao, Sarfraz Khurshid, Dewayne E. Perry |
An Incremental Approach to Scope-Bounded Checking Using a Lightweight Formal Method.  |
FM  |
2009 |
DBLP DOI BibTeX RDF |
Scope-bounded checking, computation graph, first-order logic, SAT, Alloy, white-box testing, lightweight formal method |
| 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 | 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 | Wolfgang Ahrendt, Frank S. de Boer, Immo Grabe |
Abstract Object Creation in Dynamic Logic.  |
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 | 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 | Michael Kohlhase, Johannes Lemburg, Lutz Schröder, Ewaryst Schulz |
Formal Management of CAD/CAM Processes.  |
FM  |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | Sriram K. Rajamani |
Verification, Testing and Statistics.  |
FM  |
2009 |
DBLP DOI BibTeX RDF |
|
| 1 | María Alpuente, Demis Ballis, Daniel Romero |
Specification and Verification of Web Applications in Rewriting Logic.  |
FM  |
2009 |
DBLP DOI BibTeX RDF |
|
| 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 | Christoph Lüth, Dennis Walter |
Certifiable Specification and Verification of C Programs.  |
FM  |
2009 |
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 | Olivier Ponsini, Wendelin Serwe |
A Schedulerless Semantics of TLM Models Written in SystemC Via Translation into LOTOS.  |
FM  |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Torben Amtoft, John Hatcliff, Edwin Rodríguez, Robby, Jonathan Hoag, David Greve |
Specification and Checking of Software Contracts for Conditional Information Flow.  |
FM  |
2008 |
DBLP DOI BibTeX RDF |
|
| 1 | Radu Mateescu, Damien Thivolle |
A Model Checking Language for Concurrent Value-Passing Systems.  |
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 | Thomas Noll, Stefan Rieger |
Verifying Dynamic Pointer-Manipulating Threads.  |
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 | Michael Emmi, Dimitra Giannakopoulou, Corina S. Pasareanu |
Assume-Guarantee Verification for Interface Automata.  |
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 | Engin Uzuncaova, Sarfraz Khurshid |
Constraint Prioritization for Efficient Analysis of Declarative Models.  |
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 | 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 | Irem Aktug, Mads Dam, Dilian Gurov |
Provably Correct Runtime Monitoring.  |
FM  |
2008 |
DBLP DOI BibTeX RDF |
|