Search results for "FME"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
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 Poppleton, Richard Banach	Structuring Retrenchments in B by Decomposition.	FME	2003	DBLP DOI BibTeX RDF	formal methods, refinement, decomposition, structuring, retrenchment
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	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	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	Andreas Thums, Gerhard Schellhorn	Model Checking FTA.	FME	2003	DBLP DOI BibTeX RDF	model checking, safety analysis, fault tree analysis
1	Steven P. Miller, Alan C. Tribble, Mats Per Erik Heimdahl	Proving the Shalls.	FME	2003	DBLP DOI BibTeX RDF
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	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	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	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	Alessandro Aldini, Marco Bernardo 0001	A General Approach to Deadlock Freedom Verification for Software Architectures.	FME	2003	DBLP DOI BibTeX RDF	software architecture, process algebra, deadlock
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	Giovanni Vigna	A Topological Characterization of TCP/IP Security.	FME	2003	DBLP DOI BibTeX RDF	Security, Topology, Network model, TCP/IP protocols
1	Grigore Rosu, Steven Eker, Patrick Lincoln, José Meseguer 0001	Certifying and Synthesizing Membership Equational Proofs.	FME	2003	DBLP DOI BibTeX RDF
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	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	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	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	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	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	Brian Randell	On Failures and Faults.	FME	2003	DBLP DOI BibTeX RDF	fault assumptions, Dependability, formal concepts
1	Diyaa-Addein Atiya, Steve King 0001, Jim Woodcock 0001	A Circus Semantics for Ravenscar Protected Objects.	FME	2003	DBLP DOI BibTeX RDF	Ravenscar, Ada Protected Objects, Formal Semantics, Z, Circus
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	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	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	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	Gerard J. Holzmann	Trends in Software Verification.	FME	2003	DBLP DOI BibTeX RDF
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	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 DOI BibTeX RDF
1	Colin J. Fidge	Verifying Emulation of Legacy Mission Computer Systems.	FME	2003	DBLP DOI BibTeX RDF
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	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	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	Vlad Rusu	Compositional Verification of an ATM Protocol.	FME	2003	DBLP DOI BibTeX RDF	SSCOP protocol, abstraction, theorem proving, Compositionality, PVS
1	Andreas Schäfer 0001	Combining Real-Time Model-Checking and Fault Tree Analysis.	FME	2003	DBLP DOI BibTeX RDF	Real-time systems, model-checking, fault tree analysis
1	Adolfo Duran, Ana Cavalcanti 0001, Augusto Sampaio	A Strategy for Compiling Classes, Inheritance, and Dynamic Binding.	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	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	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	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	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	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	Olga Kouchnarenko, Arnaud Lanoix	Refinement and Verification of Synchronized Component-Based Systems.	FME	2003	DBLP DOI BibTeX RDF
1	Pascal Fenkam, Harald C. 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	Toshimi Sawada, Kouichi Kishida, Kokichi Futatsugi	Past, Present, and Future of SRA Implementation of CafeOBJ: Annex.	FME	2003	DBLP DOI BibTeX RDF
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	Jean-Raymond Abrial	Event Based Sequential Program Development: Application to Constructing a Pointer Program.	FME	2003	DBLP DOI BibTeX RDF
1	Ian J. Hayes, Michael A. Jackson 0001, Cliff B. Jones	Determining the Specification of a Control System from That of Its Environment.	FME	2003	DBLP DOI BibTeX RDF
1	Vlad Rusu	Verification Using Test Generation Techniques.	FME	2002	DBLP DOI BibTeX RDF	electronic purse, Formal verification, conformance testing
1	Igor B. Bourdonov, Alexander S. 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	Natarajan Shankar	Little Engines of Proof.	FME	2002	DBLP DOI BibTeX RDF
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	Darko Marinov, Sarfraz Khurshid	VAlloy - Virtual Functions Meet a Relational Language.	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	David A. Basin	The Next 700 Synthesis Calculi.	FME	2002	DBLP DOI BibTeX RDF
1	Augusto Sampaio, Jim Woodcock 0001, Ana Cavalcanti 0001	Refinement in Circus.	FME	2002	DBLP DOI BibTeX RDF	unifying theories of programming, distribution, CSP, Z
1	Claus Pahl	Interference Analysis for Dependable Systems Using Refinement and Abstraction.	FME	2002	DBLP DOI BibTeX RDF
1	Niels Jørgensen	Safeness of Make-Based Incremental Recompilation.	FME	2002	DBLP DOI BibTeX RDF	incremental recompilation, semantic model, Make
1	Luke Wildman	A Formal Basis for a Program Compilation Proof Tool.	FME	2002	DBLP DOI BibTeX RDF
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	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	Juan Bicarregui	Do Not Read This.	FME	2002	DBLP DOI BibTeX RDF
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	Alexandre Mota 0001, Paulo Borba, Augusto Sampaio	Mechanical Abstraction of CSPZ Processes.	FME	2002	DBLP DOI BibTeX RDF
1	María Victoria Cengarle, Alexander Knapp	Towards OCL/RT.	FME	2002	DBLP DOI BibTeX RDF	Real-time systems, UML, events, OCL
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	Ana Cavalcanti 0001, 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	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	Gil Ratsaby, Baruch Sterin, Shmuel Ur	Improvements in Coverability Analysis.	FME	2002	DBLP DOI BibTeX RDF
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	Colin J. Fidge	Timing Analysis of Assembler Code Control-Flow Paths.	FME	2002	DBLP DOI BibTeX RDF
1	Michael Backes 0001, 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	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	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	Hubert Garavel, Holger Hermanns	On Combining Functional Verification and Performance Evaluation Using CADP.	FME	2002	DBLP DOI BibTeX RDF
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	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	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 DOI BibTeX RDF
1	Anthony Hall	Correctness by Construction: Integrating Formality into a Commercial Development Process.	FME	2002	DBLP DOI BibTeX RDF
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	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	Helen Treharne	Supplementing a UML Development Process with B.	FME	2002	DBLP DOI BibTeX RDF	B-Method, Stereotyping, UML Class Diagrams
1	Michael Huber, Steve King 0001	Towards an Integrated Model Checker for Railway Signalling Data.	FME	2002	DBLP DOI BibTeX RDF	Data verification, hidden formal methods, model checking
1	Vangalur S. Alagar, Zheng Xi	A Rigorous Approach to Modeling and Analyzing E-Commerce Architectures.	FME	2001	DBLP DOI BibTeX RDF
1	Jan Jürjens	Secrecy-Preserving Refinement.	FME	2001	DBLP DOI BibTeX RDF
1	Dirk Beyer 0001	Improvements in BDD-Based Reachability Analysis of Timed Automata.	FME	2001	DBLP DOI BibTeX RDF	Real-time systems, Formal verification, Timed automata, BDDs, Discretization
1	Jonathan Burton, Maciej Koutny, Giuseppe Pappalardo	Verifying Implementation Relations.	FME	2001	DBLP DOI BibTeX RDF	Behaviour ion, verification, compositionality, communicating sequential processes
1	Michael Leuschel, Thierry Massart, Andrew Currie	How to Make FDR Spin LTL Model Checking of CSP by Refinement.	FME	2001	DBLP DOI BibTeX RDF
1	Andres Flores, Richard Moore 0001, Luis Reynoso	A Formal Model of Object-Oriented Design and GoF Design Patterns.	FME	2001	DBLP DOI BibTeX RDF
1	Daniel Jackson 0001	Lightweight Formal Methods.	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	Marsha Chechik, Steve M. Easterbrook, Victor Petrovykh	Model-Checking over Multi-valued Logics.	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
1	Joseph E. Stoy, Xiaowei Shen, Arvind	Proofs of Correctness of Cache-Coherence Protocols.	FME	2001	DBLP DOI BibTeX RDF
1	Nalini Venkatasubramanian, Carolyn L. Talcott, Gul Agha	A Formal Model for Reasoning about Adaptive QoS-Enabled Middleware.	FME	2001	DBLP DOI BibTeX RDF	meta-object models, object-oriented applications, distributed systems, multimedia, theoretical foundations
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 DOI BibTeX RDF
1	Fabrice Derepas, Paul Gastin, David Plainfossé	Avoiding State Explosion for Distributed Systems with Timestamps.	FME	2001	DBLP DOI BibTeX RDF

Publications at "FME"( http://dblp.L3S.de/Venues/FME )