| Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
| 1 | Michael Goldsmith, Nick Moffat, Bill Roscoe, Tim Whitworth, Irfan Zakiuddin |
Watchdog Transformations for Property-Oriented Model-Checking.  |
FME  |
2003 |
DBLP DOI BibTeX RDF |
Watchdog Transformation, Model-Checking, Compression, CSP, FDR, State Explosion Problem |
| 1 | Julien Musset, Michaël Rusinowitch |
Computing Meta-transitions for Linear Transition Systems with Polynomials. |
FME |
2003 |
DBLP DOI BibTeX RDF |
Infinite systems, acceleration rules, model-checking, complex systems |
| 1 | Keijiro Araki, Stefania Gnesi, Dino Mandrioli (eds.) |
FME 2003: Formal Methods, International Symposium of Formal Methods Europe, Pisa, Italy, September 8-14, 2003, Proceedings |
FME |
2003 |
DBLP BibTeX RDF |
|
| 1 | Neil Henderson |
Proving the Correctness of Simpson's 4-Slot ACM Using an Assertional Rely-Guarantee Proof Method. |
FME |
2003 |
DBLP DOI BibTeX RDF |
assertion networks, asynchronous communication, rely-guarantee |
| 1 | Jin Song Dong, Jing Sun 0002, Hai H. Wang |
Checking and Reasoning about Semantic Web through Alloy. |
FME |
2003 |
DBLP DOI BibTeX RDF |
Semantic Web, Alloy |
| 1 | Ian J. Hayes, Michael A. Jackson, Cliff B. Jones |
Determining the Specification of a Control System from That of Its Environment. |
FME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Diyaa-Addein Atiya, Steve King, Jim Woodcock |
A Circus Semantics for Ravenscar Protected Objects. |
FME |
2003 |
DBLP DOI BibTeX RDF |
Ravenscar, Ada Protected Objects, Formal Semantics, Z, Circus |
| 1 | Grigore Rosu, Steven Eker, Patrick Lincoln, José Meseguer |
Certifying and Synthesizing Membership Equational Proofs. |
FME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Angelo Morzenti, Matteo Pradella, Pierluigi San Pietro, Paola Spoletini |
Model-Checking TRIO Specifications in SPIN. |
FME |
2003 |
DBLP DOI BibTeX RDF |
model checking, temporal logic, Spin, modular specifications |
| 1 | Marc Lettrari |
Using Abstractions for Heuristic State Space Exploration of Reactive Object-Oriented Systems. |
FME |
2003 |
DBLP DOI BibTeX RDF |
UML, abstractions, heuristic search, symbolic execution |
| 1 | Andreas Thums, Gerhard Schellhorn |
Model Checking FTA. |
FME |
2003 |
DBLP DOI BibTeX RDF |
model checking, safety analysis, fault tree analysis |
| 1 | Michael Poppleton, Richard Banach |
Structuring Retrenchments in B by Decomposition. |
FME |
2003 |
DBLP DOI BibTeX RDF |
formal methods, refinement, decomposition, structuring, retrenchment |
| 1 | Thomas A. Kuhn, David von Oheimb |
Interacting State Machines for Mobility. |
FME |
2003 |
DBLP DOI BibTeX RDF |
dynamic communication, boxed ambients, Interacting State Machines, verification, mobility, mobile agents, formal modeling |
| 1 | Michel Charpentier |
Composing Invariants. |
FME |
2003 |
DBLP DOI BibTeX RDF |
formal specification, temporal logic, invariants, compositional verification |
| 1 | Pascal Fenkam, Harald Gall, Mehdi Jazayeri |
Constructing Deadlock Free Event-Based Applications: A Rely/Guarantee Approach. |
FME |
2003 |
DBLP DOI BibTeX RDF |
rely/guarantee, deadlock, parallel systems, event-based systems, auxiliary variables |
| 1 | Daniele Compare, Paola Inverardi, Patrizio Pelliccione, Alessandra Sebastiani |
Integrating Model-Checking Architectural Analysis and Validation in a Real Software Life-Cycle. |
FME |
2003 |
DBLP DOI BibTeX RDF |
model checking, software development process, Architectural analysis, models consistency |
| 1 | Steven P. Miller, Alan C. Tribble, Mats Per Erik Heimdahl |
Proving the Shalls. |
FME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Patrice Chalin |
Improving JML: For a Safer and More Effective Language. |
FME |
2003 |
DBLP DOI BibTeX RDF |
behavioral interface specification languages, specification language design and semantics, arbitrary precision numeric types, assertion-based languages, formal methods, JML, Java Modeling Language |
| 1 | Giovanni Vigna |
A Topological Characterization of TCP/IP Security. |
FME |
2003 |
DBLP DOI BibTeX RDF |
Security, Topology, Network model, TCP/IP protocols |
| 1 | Alessandro Armando, Luca Compagna, Pierre Ganty |
SAT-Based Model-Checking of Security Protocols Using Planning Graph Analysis. |
FME |
2003 |
DBLP DOI BibTeX RDF |
SAT encodings, security protocols, bounded model-checking, SAT-solvers |
| 1 | Marco Bozzano, Antonella Cavallo, Massimo Cifaldi, Laura Valacca, Adolfo Villafiorita |
Improving Safety Assessment of Complex Systems: An Industrial Case Study. |
FME |
2003 |
DBLP DOI BibTeX RDF |
Formal Verification and Safety Assessment of Complex Systems, Automated Fault Tree Computation, ESACS |
| 1 | Andreas Schäfer |
Combining Real-Time Model-Checking and Fault Tree Analysis. |
FME |
2003 |
DBLP DOI BibTeX RDF |
Real-time systems, model-checking, fault tree analysis |
| 1 | Donna C. Stidolph, E. James Whitehead Jr. |
Managerial Issues for the Consideration and Use of Formal Methods. |
FME |
2003 |
DBLP DOI BibTeX RDF |
schedule, formal methods, specification, requirements, cost, Program management |
| 1 | Jei-Wen Teng, Yih-Kuen Tsay |
Composing Temporal-Logic Specifications with Machine Assistance. |
FME |
2003 |
DBLP DOI BibTeX RDF |
Assumption-Guarantee, Compositional Specification, Formal Correctness, Temporal Logic, Theorem Proving, Concurrent Systems, PVS, Compositional Verification, Component-Based Software |
| 1 | Alan Wassyng, Mark Lawford |
Lessons Learned from a Successful Implementation of Formal Methods in an Industrial Project. |
FME |
2003 |
DBLP DOI BibTeX RDF |
experience paper, verification, specification, inspection, Industrial application, safety critical software |
| 1 | Toshimi Sawada, Kouichi Kishida, Kokichi Futatsugi |
Past, Present, and Future of SRA Implementation of CafeOBJ: Annex. |
FME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Fabrice Bouquet, Bruno Legeard |
Reification of Executable Test Scripts in Formal Specicifation-Based Test Generation: The Java Card Transaction Mechanism Case Study. |
FME |
2003 |
DBLP DOI BibTeX RDF |
B abstract machine, Oracle synthesis, Representation mapping, Specification-Based test generation, Formal methods, Java Card |
| 1 | Maria-Cristina V. Marinescu, Martin C. Rinard |
A Formal Framework for Modular Synchronous System Design. |
FME |
2003 |
DBLP DOI BibTeX RDF |
modular, system design, asynchronous, formal |
| 1 | Colin J. Fidge |
Verifying Emulation of Legacy Mission Computer Systems. |
FME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Shengchao Qin, Jin Song Dong, Wei-Ngan Chin |
A Semantic Foundation for TCOZ in Unifying Theories of Programming. |
FME |
2003 |
DBLP DOI BibTeX RDF |
UTP, integrated formal specifications, semantics |
| 1 | Olga Kouchnarenko, Arnaud Lanoix |
Refinement and Verification of Synchronized Component-Based Systems. |
FME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Ewen Denney, Bernd Fischer 0002 |
Correctness of Source-Level Safety Policies. |
FME |
2003 |
DBLP DOI BibTeX RDF |
program safety, code certification, Program verification, Hoare logic, proof-carrying code |
| 1 | Amel Mammar, Régine Laleau |
Design of an Automatic Prover Dedicated to the Refinement of Database Applications. |
FME |
2003 |
DBLP DOI BibTeX RDF |
Refinement process, Proof reuse, B method, Data-intensive applications |
| 1 | Fei Xie, James C. Browne, Robert P. Kurshan |
Translation-Based Compositional Reasoning for Software Systems. |
FME |
2003 |
DBLP DOI BibTeX RDF |
Translation-based compositional reasoning, model checking, compositional reasoning, model translation |
| 1 | Michael Leuschel, Michael J. Butler |
ProB: A Model Checker for B. |
FME |
2003 |
DBLP DOI BibTeX RDF |
Model Checking, Animation, Logic Programming, Constraints, Tool Support, B-Method |
| 1 | Didier Bert, Sylvain Boulmé, Marie-Laure Potet, Antoine Requet, Laurent Voisin |
Adaptable Translator of B Specifications to Embedded C Programs. |
FME |
2003 |
DBLP DOI BibTeX RDF |
embedded systems, Code generation, smart cards, B method |
| 1 | Alessandro Aldini, Marco Bernardo |
A General Approach to Deadlock Freedom Verification for Software Architectures. |
FME |
2003 |
DBLP DOI BibTeX RDF |
software architecture, process algebra, deadlock |
| 1 | Brian Randell |
On Failures and Faults. |
FME |
2003 |
DBLP DOI BibTeX RDF |
fault assumptions, Dependability, formal concepts |
| 1 | Marc Boyer, Mihaela Sighireanu |
Synthesis and Verification of Constraints in the PGM Protocol. |
FME |
2003 |
DBLP DOI BibTeX RDF |
PGM protocol, real-time multicast protocol, finite and timed model-checking, parameterized verification, constraint synthesis |
| 1 | Marcelo F. Frias, Carlos López Pombo, Gabriel Baum, Nazareno Aguirre, T. S. E. Maibaum |
Taking Alloy to the Movies. |
FME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Adolfo Duran, Ana Cavalcanti, Augusto Sampaio |
A Strategy for Compiling Classes, Inheritance, and Dynamic Binding. |
FME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Sabine Glesner |
Program Checking with Certificates: Separating Correctness-Critical Code. |
FME |
2003 |
DBLP DOI BibTeX RDF |
safety-scalability, real-scale applications, verification, validation, certificates, correctness, program checking |
| 1 | Kouichi Kishida |
Looking Back to the Future: Thoughts on Paradigm Shift in Software Development. |
FME |
2003 |
DBLP DOI BibTeX RDF |
philosophical thoughts, software engineering, formal method, object orientation, paradigm shift |
| 1 | Lilian Burdy, Antoine Requet, Jean-Louis Lanet |
Java Applet Correctness: A Developer-Oriented Approach. |
FME |
2003 |
DBLP DOI BibTeX RDF |
Proof User Interface, Java, Correctness Proof |
| 1 | Maurice H. ter Beek, Jetty Kleijn |
Team Automata Satisfying Compositionality. |
FME |
2003 |
DBLP DOI BibTeX RDF |
team automata, synchronizations, computations, compositionality, behaviour, shuffles |
| 1 | Gerard J. Holzmann |
Trends in Software Verification. |
FME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Shengchao Qin, Wei-Ngan Chin |
Mapping Statecharts to Verilog for Hardware/Software Co-specification. |
FME |
2003 |
DBLP DOI BibTeX RDF |
operational semantics, Statecharts, homomorphism, Verilog |
| 1 | Vlad Rusu |
Compositional Verification of an ATM Protocol. |
FME |
2003 |
DBLP DOI BibTeX RDF |
SSCOP protocol, abstraction, theorem proving, Compositionality, PVS |
| 1 | Jean-Raymond Abrial |
Event Based Sequential Program Development: Application to Constructing a Pointer Program. |
FME |
2003 |
DBLP DOI BibTeX RDF |
|
| 1 | Arie Gurfinkel, Marsha Chechik |
Generating Counterexamples for Multi-valued Model-Checking. |
FME |
2003 |
DBLP DOI BibTeX RDF |
De Morgan algebras, model-checking, CTL, counterexamples, witnesses |
| 1 | Colin J. Fidge |
Timing Analysis of Assembler Code Control-Flow Paths. |
FME |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael Huber, Steve King |
Towards an Integrated Model Checker for Railway Signalling Data. |
FME |
2002 |
DBLP DOI BibTeX RDF |
Data verification, hidden formal methods, model checking |
| 1 | Vlad Rusu |
Verification Using Test Generation Techniques. |
FME |
2002 |
DBLP DOI BibTeX RDF |
electronic purse, Formal verification, conformance testing |
| 1 | Alexandre Mota, Paulo Borba, Augusto Sampaio |
Mechanical Abstraction of CSPZ Processes. |
FME |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Claus Pahl |
Interference Analysis for Dependable Systems Using Refinement and Abstraction. |
FME |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Michael W. Whalen, Johann Schumann, Bernd Fischer 0002 |
Synthesizing Certified Code. |
FME |
2002 |
DBLP DOI BibTeX RDF |
automatic program synthesis, code certification, program verification, automated theorem proving, proof-carrying code |
| 1 | Néstor Cataño, Marieke Huisman |
Formal Specification and Static Checking of Gemplus' Electronic Purse Using ESC/Java. |
FME |
2002 |
DBLP DOI BibTeX RDF |
ESC/Java, Java, specification, smart cards, static checking |
| 1 | Michael Backes, Christian Jacobi 0002, Birgit Pfitzmann |
Deriving Cryptographically Sound Implementations Using Composition and Formally Verified Bisimulation. |
FME |
2002 |
DBLP DOI BibTeX RDF |
security, cryptography, formal verification, PVS, simulatability |
| 1 | Thomas Arts, Clara Benac Earle, John Derrick |
Verifying Erlang Code: A Resource Locker Case-Study. |
FME |
2002 |
DBLP DOI BibTeX RDF |
Model checking, formal verification, process algebra, telecommunication, Erlang |
| 1 | Helen Treharne |
Supplementing a UML Development Process with B. |
FME |
2002 |
DBLP DOI BibTeX RDF |
B-Method, Stereotyping, UML Class Diagrams |
| 1 | Lars-Henrik Eriksson, Peter A. Lindsay (eds.) |
FME 2002: Formal Methods - Getting IT Right, International Symposium of Formal Methods Europe, Copenhagen, Denmark, July 22-24, 2002, Proceedings |
FME |
2002 |
DBLP BibTeX RDF |
|
| 1 | David von Oheimb, Tobias Nipkow |
Hoare Logic for NanoJava: Auxiliary Variables, Side Effects, and Virtual Methods Revisited. |
FME |
2002 |
DBLP DOI BibTeX RDF |
Java, Hoare logic, side effects, dynamic binding, Isabelle/HOL, auxiliary variables |
| 1 | Juan Bicarregui |
Do Not Read This. |
FME |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Lars Michael Kristensen, Thomas Mailund |
A Generalised Sweep-Line Method for Safety Properties. |
FME |
2002 |
DBLP DOI BibTeX RDF |
explicit state space exploration methods, state space reduction methods, practical use and tool support, reachability analysis, theoretical foundations |
| 1 | Darko Marinov, Sarfraz Khurshid |
VAlloy - Virtual Functions Meet a Relational Language. |
FME |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Bruno Legeard, Fabien Peureux, Mark Utting |
Automated Boundary Testing from Z and B. |
FME |
2002 |
DBLP DOI BibTeX RDF |
boundary values, set constraint solving, specification-based testing, B method, Z notation |
| 1 | María Victoria Cengarle, Alexander Knapp |
Towards OCL/RT. |
FME |
2002 |
DBLP DOI BibTeX RDF |
Real-time systems, UML, events, OCL |
| 1 | Jin Song Dong, Jing Sun 0002, Hai H. Wang |
Semantic Web for Extending and Linking Formalisms. |
FME |
2002 |
DBLP DOI BibTeX RDF |
specification environment, Semantic Web |
| 1 | Gil Ratsaby, Baruch Sterin, Shmuel Ur |
Improvements in Coverability Analysis. |
FME |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Luke Wildman |
A Formal Basis for a Program Compilation Proof Tool. |
FME |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Ana Cavalcanti, David A. Naumann |
Forward Simulation for Data Refinement of Classes. |
FME |
2002 |
DBLP DOI BibTeX RDF |
soundness of simulation, program analysis and verification, object-orientation, data refinement |
| 1 | Juan C. Burguillo-Rial, Manuel J. Fernández Iglesias, Francisco J. González-Castaño, Martín Llamas Nistal |
Heuristic-Driven Test Case Selection from Formal Specifications. A Case Study. |
FME |
2002 |
DBLP DOI BibTeX RDF |
heuristics for testing, risk and cost of testing, test case selection, formal testing |
| 1 | Augusto Sampaio, Jim Woodcock, Ana Cavalcanti |
Refinement in Circus. |
FME |
2002 |
DBLP DOI BibTeX RDF |
unifying theories of programming, distribution, CSP, Z |
| 1 | Natalia Ioustinova, Natalia Sidorova, Martin Steffen |
Closing Open SDL-Systems for Model Checking with DTSpin. |
FME |
2002 |
DBLP DOI BibTeX RDF |
DTSpin, open communication systems, model checking, abstractions, SDL |
| 1 | Takaaki Umedu, Yoshiki Terashima, Keiichi Yasumoto, Akio Nakata, Teruo Higashino, Kenichi Taniguchi |
A Language for Describing Wireless Mobile Applications with Dynamic Establishment of Multi-way Synchronization Channels. |
FME |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Hubert Garavel, Holger Hermanns |
On Combining Functional Verification and Performance Evaluation Using CADP. |
FME |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Neil Henderson, Stephen Paynter |
The Formal Classification and Verification of Simpson's 4-Slot Asynchronous Communication Mechanism. |
FME |
2002 |
DBLP DOI BibTeX RDF |
retrieve relation, refinement, asynchronous communication, reification |
| 1 | Thomas Firley, Ursula Goltz |
Property Dependent Abstraction of Control Structure for Software Verification. |
FME |
2002 |
DBLP DOI BibTeX RDF |
property oriented abstraction, algorithmic construction of abstract semantics, software verification |
| 1 | Ludovic Casset |
Development of an Embedded Verifier for Java Card Byte Code Using Formal Methods. |
FME |
2002 |
DBLP DOI BibTeX RDF |
Byte Code Verification, Formal Methods, B Method |
| 1 | Niels Jørgensen |
Safeness of Make-Based Incremental Recompilation. |
FME |
2002 |
DBLP DOI BibTeX RDF |
incremental recompilation, semantic model, Make |
| 1 | Anthony Hall |
Correctness by Construction: Integrating Formality into a Commercial Development Process. |
FME |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Igor B. Bourdonov, Alexander Kossatchev, Victor V. Kuliamin, Alexander K. Petrenko |
UniTesK Test Suite Architecture. |
FME |
2002 |
DBLP DOI BibTeX RDF |
automata based testing, test suite architecture, specification based testing, partition testing |
| 1 | Sharon Barner, Shoham Ben-David, Anna Gringauze, Baruch Sterin, Yaron Wolfsthal |
An Algorithmic Approach to Design Exploration. |
FME |
2002 |
DBLP DOI BibTeX RDF |
hardware debugging, hardware exploration, Model checking |
| 1 | David A. Basin |
The Next 700 Synthesis Calculi. |
FME |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Natarajan Shankar |
Little Engines of Proof. |
FME |
2002 |
DBLP DOI BibTeX RDF |
|
| 1 | Mícheál Mac an Airchinnigh |
Towards a Topos Theoretic Foundation for the Irish School of Constructive Mathematics. |
FME |
2001 |
DBLP DOI BibTeX RDF |
Topos Theory, Unifying Theory, modelling, intuitionistic logic, VDM, constructive mathematics, Heyting algebra, Cartesian closed category |
| 1 | Bernhard K. Aichernig |
Test-Case Calculation through Abstraction. |
FME |
2001 |
DBLP DOI BibTeX RDF |
test-case synthesis, abstraction rules, testing, scenarios, contract, refinement calculus |
| 1 | Marielle Doche, Isabelle Vernier-Mounier, Fabrice Kordon |
A Modular Approach to the Specification and Validation of an Electrical Flight Control System. |
FME |
2001 |
DBLP DOI BibTeX RDF |
Verification, Modularity, Test Generation, Case Tools, Heterogeneous Specification |
| 1 | Muffy Calder, Savi Maharaj, Carron Shankland |
An Adequate Logic for Full LOTOS. |
FME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Laurent Arditi, Hédi Boufaïed, Arnaud Cavanié, Vincent Stehlé |
Coverage Directed Generation of System-Level Test Cases for the Validation of a DSP System. |
FME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Leila Silva, Augusto Sampaio, Geraint Jones |
Serialising Parallel Processes in a Hardware/Software Partitioning Context. |
FME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Adnan Sherif, Augusto Sampaio, Sérgio Cavalcante |
An Integrated Approach to Specification and Validation of Real-Time Systems. |
FME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Ralf Lämmel |
Grammar Adaptation. |
FME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Jayadev Misra |
A Programming Model for Wide-Area Computing. |
FME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | José Nuno Oliveira, Pamela Zave (eds.) |
FME 2001: Formal Methods for Increasing Software Productivity, International Symposium of Formal Methods Europe, Berlin, Germany, March 12-16, 2001, Proceedings |
FME |
2001 |
DBLP BibTeX RDF |
|
| 1 | Vangalur S. Alagar, Zheng Xi |
A Rigorous Approach to Modeling and Analyzing E-Commerce Architectures. |
FME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Françoise Bellegarde, Christophe Darlot, Jacques Julliand, Olga Kouchnarenko |
Reformulation: A Way to Combine Dynamic Properties and B Refinement. |
FME |
2001 |
DBLP DOI BibTeX RDF |
Verification of PLTL properties, Combination of proof and model-checking, Refinement development |
| 1 | Marsha Chechik, Steve M. Easterbrook, Victor Petrovykh |
Model-Checking over Multi-valued Logics. |
FME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Cormac Flanagan, K. Rustan M. Leino |
Houdini, an Annotation Assistant for ESC/Java. |
FME |
2001 |
DBLP DOI BibTeX RDF |
|
| 1 | Steffen Helke, Thomas Santen |
Mechanized Analysis of Behavioral Conformance in the Eiffel Base Libraries. |
FME |
2001 |
DBLP DOI BibTeX RDF |
|
![[Valid RSS]](Pics/valid-rss.png "Validate my RSS feed")