Search results for "liveness"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
8	Nima Kaveh, Wolfgang Emmerich	Deadlock detection in distribution object systems.	ESEC / SIGSOFT FSE	2001	DBLP DOI BibTeX RDF	object middleware, model checking, UML, UML, process algebra
8	Martin Fränzle	What Will Be Eventually True of Polynomial Hybrid Automata?	TACS	2001	DBLP DOI BibTeX RDF	State recurrence, Progress properties, Verification procedures, Hybrid systems, Decidability
8	Butler W. Lampson	The ABCD's of Paxos.	PODC	2001	DBLP DOI BibTeX RDF
8	Martín Abadi	Leslie Lamport's properties and actions.	PODC	2001	DBLP DOI BibTeX RDF
8	Paritosh K. Pandya	Model Checking CTL*[DC].	TACAS	2001	DBLP DOI BibTeX RDF
8	Nina Amla, E. Allen Emerson, Kedar S. Namjoshi, Richard J. Trefler	Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams.	TACAS	2001	DBLP DOI BibTeX RDF
8	Jerzy Brzezinski, Dariusz Wawrzyniak	Consistency Requirements of Peterson's Algorithm for Mutual Exclusion of {n} Processes in a Distributed Shared Memory System.	PPAM	2001	DBLP DOI BibTeX RDF
8	Pascal Felber, Ben Jai, Rajeev Rastogi, Mark A. Smith	Using Semantic Knowledge of Distributed Objects to Increase Reliability and Availability.	WORDS	2001	DBLP DOI BibTeX RDF
8	Marie Duflot, Laurent Fribourg, Ulf Nilsson	Unavoidable Configurations of Parameterized Rings of Processes.	CONCUR	2001	DBLP DOI BibTeX RDF
8	Carole Delporte-Gallet, Hugues Fauconnier	An example of Real-Time Group Communication System.	ICDCS Workshops	2001	DBLP DOI BibTeX RDF	timed asynchronous, fault tolerance, real time, distributed algorithm
8	K. Suzanne Barber, Thomas J. Graser, Jim Holt	Providing Early Feedback in the Development Cycle Through Automated Application of Model Checking to Software Architectures.	ASE	2001	DBLP DOI BibTeX RDF
8	Heiko Mantel	Preserving Information Flow Properties under Refinement.	S&P	2001	DBLP DOI BibTeX RDF
8	Achour Mostéfaoui, Sergio Rajsbaum, Michel Raynal	Conditions on input vectors for consensus solvability in asynchronous distributed systems.	STOC	2001	DBLP DOI BibTeX RDF	fault-tolerance, consensus, asynchronous systems
8	Christian Cachin, Klaus Kursawe, Frank Petzold, Victor Shoup	Secure and Efficient Asynchronous Broadcast Protocols.	CRYPTO	2001	DBLP DOI BibTeX RDF
8	Pierfrancesco Bellini, Paolo Nesi	TILCO-X, an Extension of TILCO Temporal Logic.	ICECCS	2001	DBLP DOI BibTeX RDF	real-time systems, first order logic, verification and validation, formal specification language, temporal operators, temporal interval logic
8	Pierfrancesco Bellini, Paolo Nesi	Communicating TILCO: A Model for Real-Time System Specification.	ICECCS	2001	DBLP DOI BibTeX RDF	real-time systems, first order logic, verification and validation, formal specification language, temporal interval logic
8	Einar Broch Johnsen, Olaf Owe, Ellen Munthe-Kaas, Jüri Vain	Incremental Fault-Tolerant Design in an Object-Oriented Setting.	APAQS	2001	DBLP DOI BibTeX RDF	formal methods refinement trace semantics, Fault-tolerance, object orientation, incremental design
8	Yonit Kesten, Zohar Manna, Amir Pnueli	Verification of Clocked and Hybrid Systems.	Acta Informatica	2000	DBLP DOI BibTeX RDF
8	Abdel Mokkedem, Tim Leonard	Formal Verification of the Alpha 21364 Network Protocol.	TPHOLs	2000	DBLP DOI BibTeX RDF
8	Karsten Schmidt 0004	LoLA: A Low Level Analyser.	ICATPN	2000	DBLP DOI BibTeX RDF
8	Denis Poitrenaud, Jean-François Pradat-Peyre	Pre- and Post-agglomerations for LTL Model Checking.	ICATPN	2000	DBLP DOI BibTeX RDF
8	Jürgen Ruf, Thomas Kropf	Analyzing Real-Time Systems.	DATE	2000	DBLP DOI BibTeX RDF
8	Ken Butts	Hybrid Models for Automotive Powertrain Systems: Revisiting a Vision.	HSCC	2000	DBLP DOI BibTeX RDF
8	Yih-Kuen Tsay	Compositional Verification in Linear-Time Temporal Logic.	FoSSaCS	2000	DBLP DOI BibTeX RDF
8	Helen Treharne, Steve A. Schneider	How to Drive a B Machine.	ZB	2000	DBLP DOI BibTeX RDF	Programming Calculi, Embedded Systems, CSP, B-Method, Combining Formalisms
8	Dominique Cansell, Dominique Méry, Stephan Merz	Predicate Diagrams for the Verification of Reactive Systems.	IFM	2000	DBLP DOI BibTeX RDF
8	Kai Baukus, Saddek Bensalem, Yassine Lakhnech, Karsten Stahl	Abstracting WS1S Systems to Verify Parameterized Networks.	TACAS	2000	DBLP DOI BibTeX RDF
8	Antti Valmari	Composition and Abstraction.	MOVEP	2000	DBLP DOI BibTeX RDF
8	Jerzy Brzezinski, Dariusz Wawrzyniak	Consistency Requirements of Distributed Shared Memory for Dijkstra's Mutual Exclusion Algorithm.	ICDCS	2000	DBLP DOI BibTeX RDF	distributed shared memory, mutual exclusion, consistency models
8	Idit Keidar, Roger Khazan	A Client-Server Approach to Virtually Synchronous Group Multicast: Specifications and Algorithms.	ICDCS	2000	DBLP DOI BibTeX RDF
8	Markus Hannebauer	How to Model and Verify Concurrent Algorithms for Distributed CSPs.	CP	2000	DBLP DOI BibTeX RDF
8	Panagiotis Manolios	Correctness of Pipelined Machines.	FMCAD	2000	DBLP DOI BibTeX RDF
8	Wil Janssen, Mannes Poel, Job Zwiers	The Compositional Approach to Sequential Consistency and Lazy Caching.	Distributed Comput.	1999	DBLP DOI BibTeX RDF
8	José Ramón González de Mendívil, Federico Fariña, José Ramón Garitagoitia, Carlos F. Alastruey, José M. Bernabéu-Aubán	A Distributed Deadlock Resolution Algorithm for the AND Model.	IEEE Trans. Parallel Distributed Syst.	1999	DBLP DOI BibTeX RDF	Deadlock detection/resolution, AND model, hierarchical correctness proofs, input/output automata model, distributed systems
8	Tevfik Bultan, Richard Gerber 0001, William W. Pugh	Model-checking concurrent systems with unbounded integer variables: symbolic representations, approximations, and experimental results.	ACM Trans. Program. Lang. Syst.	1999	DBLP DOI BibTeX RDF	abstract interpretation, symbolic model checking, Presburger arithmetic
8	Zhiming Liu 0001, Mathai Joseph	Specification and Verification of Fault-Tolerance, Timing, and Scheduling.	ACM Trans. Program. Lang. Syst.	1999	DBLP DOI BibTeX RDF	schedulability, fault-tolerance, verification, real time, specification, transformation
8	Marcelo Glusman, Shmuel Katz	Mechanizing Proofs of Computation Equivalence.	CAV	1999	DBLP DOI BibTeX RDF
8	Jie Xu 0007, Brian Randell, Alexander B. Romanovsky, Robert J. Stroud, Avelino F. Zorzo, Ercument Canver, Friedrich W. von Henke	Rigorous Development of a Safety-Critical System Based on Coordinated Atomic Actions.	FTCS	1999	DBLP DOI BibTeX RDF	coordinated atomic (CA) actions, reliability and safety, model checking, Concurrency, object orientation, formal verification, exception handling, reactive systems
8	Abderrahim Benslimane, Abdelhafid Abouaissa	A Synchronization Protocol for Group Communication Systems.	MASCOTS	1999	DBLP DOI BibTeX RDF	multimedia synchroization, delta-causal order, multicast, validation, group communication system
8	Özalp Babaoglu, Renzo Davoli, Alberto Montresor	Group Communication in Partitionable Distributed Systems.	Advances in Distributed Systems	1999	DBLP DOI BibTeX RDF
8	Laura Recalde, Enrique Teruel, Manuel Silva Suárez	Autonomous Continuous P/T Systems.	ICATPN	1999	DBLP DOI BibTeX RDF
8	Jean-Michel Couvreur, Denis Poitrenaud	Detection of Illegal Behaviors Based on Unfoldings.	ICATPN	1999	DBLP DOI BibTeX RDF	Failure Equivalence, Model Checking, Petri Net, Partial Order
8	Russell Harmer, Guy McCusker	A Fully Abstract Game Semantics for Finite Nondeterminism.	LICS	1999	DBLP DOI BibTeX RDF
8	Ravi Hosabettu, Ganesh Gopalakrishnan, Mandayam K. Srivas	A Proof of Correctness of a Processor Implementing Tomasulo's Algorithm without a Reorder Buffer.	CHARME	1999	DBLP DOI BibTeX RDF
8	Vugranam C. Sreedhar, Roy Dz-Ching Ju, David M. Gillies, Vatsa Santhanam	Translating Out of Static Single Assignment Form.	SAS	1999	DBLP DOI BibTeX RDF
8	Rana Barua, Suman Roy 0001, Zhou Chaochen	Completeness of Neighbourhood Logic.	STACS	1999	DBLP DOI BibTeX RDF
8	Giorgio Delzanno, Andreas Podelski	Model Checking in CLP.	TACAS	1999	DBLP DOI BibTeX RDF
8	Carole Delporte-Gallet, Hugues Fauconnier	Real-Time Fault-Tolerant Atomic Broadcast.	SRDS	1999	DBLP DOI BibTeX RDF	real-time distributed algorithms, fault-tolerance, atomic broadcast, partial synchrony
8	Jesús E. Villadangos, Federico Fariña, José Ramón González de Mendívil, José Ramón Garitagoitia, José M. Bernabéu-Aubán, Gottfried Vossen	Resolving Distributed Deadlocks in the OR Request Model.	SRDS	1999	DBLP DOI BibTeX RDF
8	Christel Baier, Marta Z. Kwiatkowska	Model Checking for a Probabilistic Branching Time Logic with Fairness.	Distributed Comput.	1998	DBLP DOI BibTeX RDF	Probabilistic processes, Verification, Temporal logic, Fairness
8	Mihaela Sighireanu, Radu Mateescu 0001	Verification of the Link Layer Protocol of the IEEE-1394 Serial Bus (FireWire): An Experiment with E-LOTOS.	Int. J. Softw. Tools Technol. Transf.	1998	DBLP DOI BibTeX RDF
8	Boutheina Chetali	Formal Verification of Concurrent Programs Using the Larch Prover.	IEEE Trans. Software Eng.	1998	DBLP DOI BibTeX RDF	theorem prover methodology, Larch prover, computer-checked proof, Formal verification, communication protocol, protocol verification, UNITY
8	Chris M. N. Tofts, Graham M. Birtwistle	A Denotational Semantics for a Process-Based Simulation Language.	ACM Trans. Model. Comput. Simul.	1998	DBLP DOI BibTeX RDF
8	Rajeev Alur, Thomas A. Henzinger	Finitary Fairness.	ACM Trans. Program. Lang. Syst.	1998	DBLP DOI BibTeX RDF	modeling of asynchronous systems, fairness, program verification, distributed consensus
8	Claus Aßmann	Performance Results for an Implementation of the Process Coordination Language K2.	IFL	1998	DBLP DOI BibTeX RDF	Petri nets, coordination language, concurrent computing, performance results
8	Amar Bouali	XEVE, an ESTEREL Verification Environment.	CAV	1998	DBLP DOI BibTeX RDF
8	Ying Xu, Eduard Cerny, Xiaoyu Song, Francisco Corella, Otmane Aït Mohamed	Model Checking for a First-Order Temporal Logic Using Multiway Decision Graphs.	CAV	1998	DBLP DOI BibTeX RDF
8	Paul B. Jackson	Verifying a Garbage Collection Algorithm.	TPHOLs	1998	DBLP DOI BibTeX RDF
8	Jürgen Dingel	A Trace-Based Refinement Calculus for Shared-Variable Parallel Programs.	AMAST	1998	DBLP DOI BibTeX RDF
8	Virgil D. Gligor, Serban I. Gavrila	Application-Oriented Security Policies and Their Composition (Position Paper).	Security Protocols Workshop	1998	DBLP DOI BibTeX RDF
8	Luc Moreau 0001	A Distributed Garbage Collector with Diffusion Tree Reorganisation and Mobile Objects.	ICFP	1998	DBLP DOI BibTeX RDF
8	Yoshinao Isobe, Yutaka Sato, Kazuhito Ohmaki	Eventuality in LOTOS with a Disjunction Operator.	ASIAN	1998	DBLP DOI BibTeX RDF
8	Luca Aceto, Augusto Burgueño, Kim Guldstrand Larsen	Model Checking via Reachability Testing for Timed Automata.	TACAS	1998	DBLP DOI BibTeX RDF
8	Gurdip Singh, I. Buricea, Zhenyu Mao	Composition of Service Specifications.	ICNP	1998	DBLP DOI BibTeX RDF
8	Jianping Lu, Sofiène Tahar	Practical Approaches to the Automatic Verification of an ATM Switch Fabric Using VIS.	Great Lakes Symposium on VLSI	1998	DBLP DOI BibTeX RDF
8	Ernie Cohen, Leslie Lamport	Reduction in TLA.	CONCUR	1998	DBLP DOI BibTeX RDF
8	Darren George Priddin, Alan Burns 0001	Integrating Real-Time Structured Design and Formal Techniques.	FTRTFT	1998	DBLP DOI BibTeX RDF
8	Bernhard Möller	Idel Stream Algebra.	Prospects for Hardware Foundations	1998	DBLP DOI BibTeX RDF
8	Fong Pong, Michel Dubois 0001	Verification Techniques for Cache Coherence Protocols.	ACM Comput. Surv.	1997	DBLP DOI BibTeX RDF	state representation and expansion, finite state machine, shared-memory multiprocessors, cache coherence, protocol verification
8	Michael von der Beeck, Tiziana Margaria, Bernhard Steffen	A formal requirements engineering method for specification, synthesis, and verification.	SEE	1997	DBLP DOI BibTeX RDF
8	Tevfik Bultan, Richard Gerber 0001, William W. Pugh	Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetic.	CAV	1997	DBLP DOI BibTeX RDF
8	Karsten Schmidt 0004	Siphons, Traps and High-Level Nets with Infinite Color Domains.	ICATPN	1997	DBLP DOI BibTeX RDF	THEORY: Analysis and synthesis, Higher-level net models, structure and behaviour of nets
8	Falko Bause	Analysis of Petri Nets with a Dynamic Priority Method.	ICATPN	1997	DBLP DOI BibTeX RDF
8	Alberto Faro, Daniela Giordano	A Theory of Interactions and Scenes for User Centered Systems Specification and Verification.	APSEC	1997	DBLP DOI BibTeX RDF	situated action calculus, interactive systems verification, Requirements engineering
8	Grégory Duval, Thierry Cattel	From Architecture Down to Implementation of Safe Process Control Applications.	HICSS (1)	1997	DBLP DOI BibTeX RDF
8	Thomas A. Henzinger, Orna Kupferman, Sriram K. Rajamani	Fair Simulation.	CONCUR	1997	DBLP DOI BibTeX RDF
8	Zhou Chaochen, Michael R. Hansen	An Adequate First Order Interval Logic.	COMPOS	1997	DBLP DOI BibTeX RDF
8	Ben C. Moszkowski	Compositional Reasoning Using Interval Temporal Logic and Tempura.	COMPOS	1997	DBLP DOI BibTeX RDF
8	Fabien Coelho	Compiling Dynamic Mappings with Array Copies.	PPoPP	1997	DBLP DOI BibTeX RDF	FORTRAN
8	E. J. Younger, Keith H. Bennett, Z. Luo	A Formal Transformation and Refinement Method for Concurrent Programs.	ICSM	1997	DBLP DOI BibTeX RDF	Concurrency, program transformations, re-engineering
8	Guoping Jia, Guoliang Zheng	Fair Transition System Specification: An Integrated Approach.	ACM SIGPLAN Notices	1996	DBLP DOI BibTeX RDF
8	Rajeev Alur, Thomas A. Henzinger, Pei-Hsin Ho	Automatic Symbolic Verification of Embedded Systems.	IEEE Trans. Software Eng.	1996	DBLP DOI BibTeX RDF	real-time and hybrid systems, model checking, temporal logic, symbolic analysis, Specification and verification
8	John McLean	A General Theory of Composition for a Class of "Possibilistic'' Properties.	IEEE Trans. Software Eng.	1996	DBLP DOI BibTeX RDF	composition, Computer security, information flow, security models
8	Jens Knoop, Bernhard Steffen, Jürgen Vollmer 0001	Parallelism for Free: Efficient and Optimal Bitvector Analyses for Parallel Programs.	ACM Trans. Program. Lang. Syst.	1996	DBLP DOI BibTeX RDF	assignment motion, bitvector problems, definition-use chains, partial dead-code elimination, parallelism, synchronization, shared memory, data flow analysis, program optimization, code motion, strength reduction, interleaving semantics
8	Kunihiko Hiraishi	Reducted State Space Representation for Unbounded Vector State Spaces.	Application and Theory of Petri Nets	1996	DBLP DOI BibTeX RDF
8	Tevfik Bultan, Jeffrey Fischer, Richard Gerber 0001	Compositional Verification by Model Checking for Counter-Examples.	ISSTA	1996	DBLP DOI BibTeX RDF
8	Paolo Ciancarini, Cecilia Mascolo	Analyzing the Dynamics of a Z Specification.	DISCO	1996	DBLP DOI BibTeX RDF
8	David A. Schmidt	Abstract Interpretation of Small-Step Semantics.	LOMAPS	1996	DBLP DOI BibTeX RDF
8	Dirk Grunwald, Richard Neves	Whole-Program Optimization for Time and Space Efficient Threads.	ASPLOS	1996	DBLP DOI BibTeX RDF
8	Hermann von Issendorff	Time and Logic: A Calculus of Binary Events.	Computing	1995	DBLP DOI BibTeX RDF	causality and time, time-bound propositions, three-valued algebra, processing logic, Theory of computation
8	Jürgen Dingel, Thomas Filkorn	Model Checking for Infinite State Systems Using Data Abstraction, Assumption-Commitment Style reasoning and Theorem Proving.	CAV	1995	DBLP DOI BibTeX RDF
8	David L. Dill, Howard Wong-Toi	Verification of Real-Time Systems by Successive Over and Under Approximation.	CAV	1995	DBLP DOI BibTeX RDF
8	Holger Busch	A Practical Method for Reasoning about Distributed Systems in a Theorem Prover.	TPHOLs	1995	DBLP DOI BibTeX RDF
8	Thomas A. Henzinger, Peter W. Kopke, Howard Wong-Toi	The Expressive Power of Clocks.	ICALP	1995	DBLP DOI BibTeX RDF
8	Peter Baumann, Karl Lermer	A Framework for the Specification of Reactive and Concurrent Systems in Z.	FSTTCS	1995	DBLP DOI BibTeX RDF	formal methods, reactive systems, Z, TLA
8	Ben C. Moszkowski	Compositional reasoning about projected and infinite time.	ICECCS	1995	DBLP DOI BibTeX RDF	multiple time granularities, parallel programming, concurrency, temporal logic, temporal logic, concurrency control, theorem proving, multiprocessing systems, deadlock, commitments, concurrent system, assumptions, Interval Temporal Logic
8	Kimon P. Valavanis, Srinivasan Ramaswamy, Steve P. Landry	Extended Petri net-based modeling, analysis and simulation of an intelligent materials handling system.	J. Intell. Robotic Syst.	1994	DBLP DOI BibTeX RDF	Intelligent materials handling system, diagnostic intelligence, extended Petri nets, hierarchical decomposition
8	Fei-Yue Wang 0001, Michael Mittmann, George N. Saridis	Coordination specification for CIRSSE robotic platform system using Petri net transducers.	J. Intell. Robotic Syst.	1994	DBLP DOI BibTeX RDF	Petri net transducer, coordination structure, intelligent machines, communication, command language
8	Jerry R. Burch, Edmund M. Clarke, David E. Long, Kenneth L. McMillan, David L. Dill	Symbolic model checking for sequential circuit verification.	IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.	1994	DBLP DOI BibTeX RDF
8	Enrique Teruel, Manuel Silva Suárez	Well-Formedness of Equal Conflict Systems.	Application and Theory of Petri Nets	1994	DBLP DOI BibTeX RDF	Place/Transition net systems, Rank theorem, Well-formedness, Decomposition, Structure theory