Search results for "Safety properties"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
3	Eran Yahav, G. Ramalingam	Verifying safety properties using separation and heterogeneous abstractions.	PLDI	2004	DBLP DOI BibTeX RDF	typestate verification, verification, program analysis, abstract interpretation, safety properties
3	Shing-Chi Cheung, Jeff Kramer	Checking Safety Properties Using Compositional Reachability Analysis.	ACM Trans. Softw. Eng. Methodol.	1999	DBLP DOI BibTeX RDF	compositional reachability analysis, distributed systems, model checking, static analysis, safety properties
3	Laura K. Dillon	Verifying General Safety Properties of Ada Tasking Programs.	IEEE Trans. Software Eng.	1990	DBLP DOI BibTeX RDF	safety properties verification, Ada tasking programs, isolation approach, automating partial correctness proofs, Ada, program verification, concurrent programs, deadlock, mutual exclusion, symbolic execution, multiprocessing programs
2	Tuomas Launiainen, Keijo Heljanko, Tommi A. Junttila	Efficient Model Checking of PSL Safety Properties.	ACSD	2010	DBLP DOI BibTeX RDF	model checking, safety properties, PSL, NuSMV
2	Ariel Cohen 0002, Kedar S. Namjoshi	Local proofs for global safety properties.	Formal Methods in System Design	2009	DBLP DOI BibTeX RDF	Local proofs, Model checking, Compositionality, Local reasoning
2	Erion Plaku, Lydia E. Kavraki, Moshe Y. Vardi	Falsification of LTL Safety Properties in Hybrid Systems.	TACAS	2009	DBLP DOI BibTeX RDF
2	Lucia Acciai, Michele Boreale	Deciding Safety Properties in Infinite-State Pi-Calculus via Behavioural Types.	ICALP	2009	DBLP DOI BibTeX RDF	behavioural types, safety, decidability, pi-calculus, spatial logic
2	Rohit Chadha, Carl A. Gunter, José Meseguer, Ravinder Shankesi, Mahesh Viswanathan	Modular Preservation of Safety Properties by Cookie-Based DoS-Protection Wrappers.	FMOODS	2008	DBLP DOI BibTeX RDF
2	Grigore Rosu, Feng Chen, Thomas Ball	Synthesizing Monitors for Safety Properties: This Time with Calls and Returns.	RV	2008	DBLP DOI BibTeX RDF
2	Guy Edward Gallasch, Jonathan Billington, Somsak Vanit-Anunchai, Lars Michael Kristensen	Checking safety properties on-the-fly with the sweep-line method.	STTT	2007	DBLP DOI BibTeX RDF	Sweep-line method, On-the-fly model checking, Datagram Congestion Control Protocol
2	Ariel Cohen 0002, Kedar S. Namjoshi	Local Proofs for Global Safety Properties.	CAV	2007	DBLP DOI BibTeX RDF
2	Orna Kupferman, Robby Lampert	On the Construction of Fine Automata for Safety Properties.	ATVA	2006	DBLP DOI BibTeX RDF
2	Shinya Umeno, Nancy A. Lynch	Proving Safety Properties of an Aircraft Landing Protocol Using I/O Automata and the PVS Theorem Prover: A Case Study.	FM	2006	DBLP DOI BibTeX RDF
2	Fabrice Bouquet, Frédéric Dadeau, Julien Groslambert, Jacques Julliand	Safety Property Driven Test Generation from.	FATES/RV	2006	DBLP DOI BibTeX RDF	JavaCard, automated testing, black-box testing, safety properties, Java Modeling Language
2	David Cachera, Katell Morin-Allory	Verification of safety properties for parameterized regular systems.	ACM Trans. Embedded Comput. Syst.	2005	DBLP DOI BibTeX RDF	regular systems, embedded systems, codesign, Polyhedral model, parameterized systems
2	Vlad Rusu, Hervé Marchand, Thierry Jéron	Automatic Verification and Conformance Testing for Validating Safety Properties of Reactive Systems.	FM	2005	DBLP DOI BibTeX RDF	symbolic test generation, verification, conformance testing
2	Zurab Khasidashvili, Alexander Nadel, Amit Palti, Ziyad Hanna	Simultaneous SAT-Based Model Checking of Safety Properties.	Haifa Verification Conference	2005	DBLP DOI BibTeX RDF
2	Jon A. Solworth, Robert H. Sloan	A Layered Design of Discretionary Access Controls with Decidable Safety Properties.	IEEE Symposium on Security and Privacy	2004	DBLP DOI BibTeX RDF
2	Abhay Vardhan, Koushik Sen, Mahesh Viswanathan, Gul Agha	Learning to Verify Safety Properties.	ICFEM	2004	DBLP DOI BibTeX RDF
2	Dachuan Yu, Zhong Shao	Verification of safety properties for concurrent assembly code.	ICFP	2004	DBLP DOI BibTeX RDF	local guarantee, concurrency, assembly
2	Reiner Hähnle, Wojciech Mostowski	Verification of Safety Properties in the Presence of Transactions.	CASSIS	2004	DBLP DOI BibTeX RDF
2	John Cochran, Deepak Kapur, Darko Stefanovic	Model Checking Reconfigurable Processor Configurations for Safety Properties.	FPL	2003	DBLP DOI BibTeX RDF
2	Marko Mäkelä	Model Checking Safety Properties in Modular High-Level Nets.	ICATPN	2003	DBLP DOI BibTeX RDF	state space enumeration, model checking, modular systems, high-level nets
2	Timo Latvala	Efficient Model Checking of Safety Properties.	SPIN	2003	DBLP DOI BibTeX RDF
2	Ran Shaham, Eran Yahav, Elliot K. Kolodner, Shmuel Sagiv	Establishing Local Temporal Heap Safety Properties with Applications to Compile-Time Memory Management.	SAS	2003	DBLP DOI BibTeX RDF
2	Shlomi Dolev, Frank A. Stomp	Safety assurance via on-line monitoring.	Distributed Computing	2003	DBLP DOI BibTeX RDF	Distributed systems, Monitors, Safety properties
2	John Håkansson, Bengt Jonsson, Ola Lundqvist	Generating online test oracles from temporal logic specifications.	STTT	2003	DBLP DOI BibTeX RDF	Online test oracles, Temporal logic specifications, Case studies, Safety properties, Metric temporal logic
2	M. Edwin Johnson	Model Checking Safety Properties of Servo-Loop Control Systems.	DSN	2002	DBLP DOI BibTeX RDF
2	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
2	Charles Hymans	Checking Safety Properties of Behavioral VHDL Descriptions by Abstract Interpretation.	SAS	2002	DBLP DOI BibTeX RDF
2	Eran Yahav	Verifying safety properties of concurrent Java programs using 3-valued logic.	POPL	2001	DBLP DOI BibTeX RDF	Java
2	Thomas Ball, Sriram K. Rajamani	Automatically Validating Temporal Safety Properties of Interfaces.	SPIN	2001	DBLP DOI BibTeX RDF
2	Monika Maidl	A Unifying Model Checking Approach for Safety Properties of Parameterized Systems.	CAV	2001	DBLP DOI BibTeX RDF
2	Paul Ammann, Wei Ding 0003, Daling Xu	Using a Model Checker to Test Safety Properties.	ICECCS	2001	DBLP DOI BibTeX RDF	Model checking, Software testing, Safety, Mutation analysis
2	Peter Thiemann	Enforcing Safety Properties Using Type Specialization.	ESOP	2001	DBLP DOI BibTeX RDF
2	Mary Sheeran, Satnam Singh, Gunnar Stålmarck	Checking Safety Properties Using Induction and a SAT-Solver.	FMCAD	2000	DBLP DOI BibTeX RDF
2	Julia Padberg, Kathrin Hoffmann, Magdalena Gajewsky	Stepwise Introduction and Preservation of Safety Properties in Algebraic High-Level Net Systems.	FASE	2000	DBLP DOI BibTeX RDF
2	Hiromi Hiraishi	Verification of deadlock free property of high level robot control.	Asian Test Symposium	2000	DBLP DOI BibTeX RDF	deadlock free property, high level robot control, verification algorithm, task control architecture, concurrent robot control processes, symbolic model verifier, symbolic model checking algorithm, robots, formal verification, logic testing, concurrency control, message passing, symbol manipulation, safety properties, liveness properties
2	Vlad Rusu, Eli Singerman	On Proving Safety Properties by Integrating Static Analysis, Theorem Proving and Abstraction.	TACAS	1999	DBLP DOI BibTeX RDF
2	Armin Biere, Edmund M. Clarke, Richard Raimi, Yunshan Zhu	Verifiying Safety Properties of a Power PC Microprocessor Using Symbolic Model Checking without BDDs.	CAV	1999	DBLP DOI BibTeX RDF
2	Orna Kupferman, Moshe Y. Vardi	Model Checking of Safety Properties.	CAV	1999	DBLP DOI BibTeX RDF
2	Julia Padberg, Magdalena Gajewsky, Claudia Ermel	Rule-Based Refinement of High-Level Nets Preserving Safety Properties.	FASE	1998	DBLP DOI BibTeX RDF
2	Vincent David, Jean Delcoigne, Evelyne Leret, Alain Ourghanlian, Philippe Hilsenkopf, Philippe Paris	Safety Properties Ensured by the OASIS Model for Safety Critical Real-Time Systems.	SAFECOMP	1998	DBLP DOI BibTeX RDF
2	Laurent Fribourg, Hans Olsén	Proving Safety Properties of Infinite State Systems by Compilation into Presburger Arithmetic.	CONCUR	1997	DBLP DOI BibTeX RDF
2	J. Boulanger, V. Delebarre, Stéphane Natkin, J. Ozello	Deriving Safety Properties of Critical Software from the System Risk Analysis Application to Ground Transportation Systems. (PDF / PS)	HASE	1997	DBLP DOI BibTeX RDF
2	Rafael Ramirez	A logical approach for specification and execution of concurrent real-time systems.	RTCSA	1997	DBLP DOI BibTeX RDF	logical approach, concurrent real time system specification, declarative logic programming based language, concurrent real time programming, procedural interpretation, concurrent programming paradigms, kernel language, concurrent real time object oriented framework, correctness, temporal constraints, safety properties, logic programming languages, time requirements
2	Kyo Chul Kang, Kwang-Il Ko	Formalization and Verification of Safety Properties of Statechart Specifications.	APSEC	1996	DBLP DOI BibTeX RDF	real-time system, temporal logic, Statecharts, safety property, specification technique, reachability graph
2	Shing-Chi Cheung, Jeff Kramer	Checking Subsystem Safety Properties in Compositional Reachability Analysis.	ICSE	1996	DBLP BibTeX RDF	automated method, compositional reachability analysis, evolutionary change, gas station system, globally observable actions, hierarchical subsystem composition, safety property violation, subsystem safety property checking, undefined state, software engineering, software architecture, software developers, distributed processing, program analysis, finite state machines, finite-state machines, safety, distributed program, reachability analysis, program diagnostics, interacting processes
2	Bengt Jonsson, Lars Kempe	Verifying Safety Properties of a Class of Infinite-State Distributed Algorithms.	CAV	1995	DBLP DOI BibTeX RDF
2	Xudong He	A method for analyzing properties of hierarchical predicate transition nets. (PDF / PS)	COMPSAC	1995	DBLP DOI BibTeX RDF	hierarchical predicate transition nets, hierarchical high level Petri nets, distributed systems modelling, hierarchical predicate transition Petri nets, temporal induction techniques, hybrid reasoning technique, net structural reasoning, behavioral reasoning, first order logic reasoning, formal method, Petri nets, distributed processing, inference mechanisms, formal logic, safety properties, liveness properties
2	Jennifer Widom, David Gries, Fred B. Schneider	Trace-Based Network Proof Systems: Expressiveness and Completeness.	ACM Trans. Program. Lang. Syst.	1992	DBLP DOI BibTeX RDF	trace logics, temporal logics, safety properties, process networks
2	Patrice Godefroid, Pierre Wolper	Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties.	CAV	1991	DBLP DOI BibTeX RDF
2	Jerry R. Burch	Verifying Liveness Properties by Verifying Safety Properties.	CAV	1990	DBLP DOI BibTeX RDF
2	Peter Grønning, Thomas Qvist Nielsen, Hans Henrik Løvengreen	Refinement and Composition of Transition-based Rely-Guarantee Specification with Auxiliary Variables.	FSTTCS	1990	DBLP DOI BibTeX RDF	Rely-guarantee specification, transition systems, compositional verification, safety properties, shared variables
1	Jan Magott, Pawel Skrobanek	Timing analysis of safety properties using fault trees with time dependencies and timed state-charts.	Rel. Eng. & Sys. Safety	2012	DBLP DOI BibTeX RDF
1	Lucia Acciai, Michele Boreale	Deciding safety properties in infinite-state pi-calculus via behavioural types.	Inf. Comput.	2012	DBLP DOI BibTeX RDF
1	Werner Damm, Carsten Ihlemann, Viorica Sofronie-Stokkermans	PTIME Parametric Verification of Safety Properties for Reasonable Linear Hybrid Automata.	Mathematics in Computer Science	2011	DBLP DOI BibTeX RDF
1	Giorgio Delzanno, Arnaud Sangnier, Gianluigi Zavattaro	Parameterized Verification of Safety Properties in Ad Hoc Network Protocols	PACO	2011	DBLP DOI BibTeX RDF
1	Tuomas Launiainen, Keijo Heljanko, Tommi A. Junttila	Efficient model checking of PSL safety properties.	IET Computers & Digital Techniques	2011	DBLP DOI BibTeX RDF
1	Siavash Soleimanifard, Dilian Gurov, Marieke Huisman	ProMoVer: Modular Verification of Temporal Safety Properties.	SEFM	2011	DBLP DOI BibTeX RDF
1	Étienne André, Romain Soulat	Synthesis of Timing Parameters Satisfying Safety Properties.	RP	2011	DBLP DOI BibTeX RDF
1	Werner Damm, Carsten Ihlemann, Viorica Sofronie-Stokkermans	Decidability and complexity for the verification of safety properties of reasonable linear hybrid automata.	HSCC	2011	DBLP DOI BibTeX RDF
1	Camilo Rocha, José Meseguer	Proving Safety Properties of Rewrite Theories.	CALCO	2011	DBLP DOI BibTeX RDF
1	Wihem Arsac, Luca Compagna, Samuel Paul Kaluvuri, Serena Elisa Ponta	Security validation tool for business processes.	SACMAT	2011	DBLP DOI BibTeX RDF
1	Eran Yahav, Mooly Sagiv	Verifying safety properties of concurrent heap-manipulating programs.	ACM Trans. Program. Lang. Syst.	2010	DBLP DOI BibTeX RDF
1	Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz	Verifying Safety Properties With the TLA+ Proof System	CoRR	2010	DBLP BibTeX RDF
1	Xiaofang Chen, Yu Yang, Ganesh Gopalakrishnan, Ching-Tsun Chou	Efficient methods for formally verifying safety properties of hierarchical cache coherence protocols.	Formal Methods in System Design	2010	DBLP DOI BibTeX RDF
1	Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz	Verifying Safety Properties with the TLA+ Proof System.	IJCAR	2010	DBLP DOI BibTeX RDF
1	Hind Alotaibi, Hussein Zedan	Runtime verification of safety properties in multi-agents systems.	ISDA	2010	DBLP DOI BibTeX RDF
1	Marieke Huisman, Dilian Gurov	CVPP: A Tool Set for Compositional Verification of Control-Flow Safety Properties.	FoVeOOS	2010	DBLP DOI BibTeX RDF
1	Parisa Heidari, Hanifa Boucheneb	Efficient Method for Checking the Existence of a Safety/ Reachability Controller for Time Petri Nets.	ACSD	2010	DBLP DOI BibTeX RDF	on-the-fly algorithm, reachability properties, time Petri nets, safety properties, controller synthesis
1	Azer Bestavros, Assaf J. Kfoury, Andrei Lapets, Michael J. Ocean	Safe compositional network sketches: formal framework.	HSCC	2010	DBLP DOI BibTeX RDF	modeling, design, verification, typing, compositionality
1	Mark Gabel, Zhendong Su	Online inference and enforcement of temporal properties.	ICSE	2010	DBLP DOI BibTeX RDF	online algorithm, dynamic analysis, temporal properties
1	William R. Harris, Sriram Sankaranarayanan, Franjo Ivancic, Aarti Gupta	Program analysis via satisfiability modulo path programs.	POPL	2010	DBLP DOI BibTeX RDF	program analysis, abstract interpretation, symbolic execution, path sensitivity, smt solvers, satisfiability solvers
1	Patrick Maxim Rondon, Ming Kawaguchi, Ranjit Jhala	Low-level liquid types.	POPL	2010	DBLP DOI BibTeX RDF	liquid types, c, type inference, dependent types
1	Paul Attasara-Mason	An Axiomatic and Object-Based Approach to Tracing Safety Properties in the Context of ARP 4754.	IAIT	2009	DBLP DOI BibTeX RDF
1	Mohsen Khaxar, Saeed Jalili, Narges Khakpour, M. Shaban Jokhio	Monitoring safety properties of composite web services at runtime using CSP.	EDOCW	2009	DBLP DOI BibTeX RDF
1	Erion Plaku, Lydia E. Kavraki, Moshe Y. Vardi	Hybrid systems: from verification to falsification by combining motion planning and discrete search.	Formal Methods in System Design	2009	DBLP DOI BibTeX RDF	Discrete search, Sampling-based planning, Hybrid system, Decomposition, Safety properties, Nonlinear dynamics, Robot motion planning
1	Kyu Il Kim, Won Gil Choi, Eun-Ju Lee, Ung-Mo Kim	RBAC-based access control for privacy protection in pervasive environments.	ICUIMC	2009	DBLP DOI BibTeX RDF	privacy, access control, RBAC, pervasive environments
1	Sumit Gulwani, Sagar Jain, Eric Koskinen	Control-flow refinement and progress invariants for bound analysis.	PLDI	2009	DBLP DOI BibTeX RDF	control-flow refinement, progress invariants, formal verification, program verification, termination, bound analysis
1	Nathan Grasso Bronson, Christos Kozyrakis, Kunle Olukotun	Feedback-directed barrier optimization in a strongly isolated STM.	POPL	2009	DBLP DOI BibTeX RDF	bytecode rewriting, deoptimization, strong isolation, weak isolation, transactional memory, hot swap
1	Pierre Ganty, Rupak Majumdar, Andrey Rybalchenko	Verifying liveness for asynchronous programs.	POPL	2009	DBLP DOI BibTeX RDF	asynchronous (event-driven) programming, fair termination, petri nets, liveness
1	Lukasz Ziarek, Suresh Jagannathan, Matthew Fluet, Umut A. Acar	Speculative N-Way barriers.	DAMP	2009	DBLP DOI BibTeX RDF	fork/join execution, n-way barriers, speculation, multi-threaded programs
1	Anh Vo, Sarvani S. Vakkalanka, Michael Delisi, Ganesh Gopalakrishnan, Robert M. Kirby, Rajeev Thakur	Formal verification of practical MPI programs.	PPOPP	2009	DBLP DOI BibTeX RDF	dynamic partial order reduction, model checking, message passing interface, distributed programming, mpi
1	Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, Simon Winwood	seL4: formal verification of an OS kernel.	SOSP	2009	DBLP DOI BibTeX RDF	l4, sel4, microkernel, isabelle/hol
1	Xavier Leroy	Formal verification of a realistic compiler.	Commun. ACM	2009	DBLP DOI BibTeX RDF
1	Stavros Tripakis	Checking timed Büchi automata emptiness on simulation graphs.	ACM Trans. Comput. Log.	2009	DBLP DOI BibTeX RDF	property-preserving abstractions, timed Büchi automata, model checking, Formal methods, specification languages
1	Gilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk	Certificate translation for optimizing compilers.	ACM Trans. Program. Lang. Syst.	2009	DBLP DOI BibTeX RDF	static analysis, program verification, program optimizations, Proof-carrying code
1	Subodh Sharma, Ganesh Gopalakrishnan, Eric Mercer, Jim Holt	MCC: A runtime verification tool for MCAPI user applications.	FMCAD	2009	DBLP DOI BibTeX RDF
1	Sebastián Uchitel, Greg Brunet, Marsha Chechik	Synthesis of Partial Behavior Models from Properties and Scenarios.	IEEE Trans. Software Eng.	2009	DBLP DOI BibTeX RDF
1	Juan Antonio Navarro Pérez, Andrey Rybalchenko, Atul Singh	Cardinality Abstraction for Declarative Networking Applications.	CAV	2009	DBLP DOI BibTeX RDF
1	Joxan Jaffar, Andrew E. Santosa	Recursive Abstractions for Parameterized Systems.	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	Chao Wang, Sudipta Kundu, Malay K. Ganai, Aarti Gupta	Symbolic Predictive Analysis for Concurrent Programs.	FM	2009	DBLP DOI BibTeX RDF
1	Pierre Ganty, Rupak Majumdar	Analyzing Real-Time Event-Driven Programs.	FORMATS	2009	DBLP DOI BibTeX RDF
1	Shinya Umeno	Machine-Assisted Parameter Synthesis of the Biphase Mark Protocol Using Event Order Abstraction.	FORMATS	2009	DBLP DOI BibTeX RDF
1	Naghmeh Ghafari, Arie Gurfinkel, Richard J. Trefler	Verification of Parameterized Systems with Combinations of Abstract Domains.	FMOODS/FORTE	2009	DBLP DOI BibTeX RDF
1	Jean-Michel Contet, Franck Gechter, Pablo Gruer, Abderrafiaa Koukam	Bending Virtual Spring-Damper: A Solution to Improve Local Platoon Control.	ICCS	2009	DBLP DOI BibTeX RDF	local control, stability proof, simulation, Platoon
1	David Hardin, T. Douglas Hiratzka, D. Randolph Johnson, Lucas Wagner, Michael W. Whalen	Development of Security Software: A High Assurance Methodology.	ICFEM	2009	DBLP DOI BibTeX RDF
1	Thai Son Hoang, Hironobu Kuruma, David A. Basin, Jean-Raymond Abrial	Developing Topology Discovery in Event-B.	IFM	2009	DBLP DOI BibTeX RDF