Search results for "LTL"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
24	Lubos Brim, Ivana Cerná, Pavel Krcál, Radek Pelánek	Distributed LTL Model Checking Based on Negative Cycle Detection.	FSTTCS	2001	DBLP DOI BibTeX RDF
24	Jean-Michel Couvreur, Sébastien Grivet, Denis Poitrenaud	Designing a LTL Model-Checker Based on Unfolding Graphs.	ICATPN	2000	DBLP DOI BibTeX RDF
24	Javier Esparza, Keijo Heljanko	A New Unfolding Approach to LTL Model Checking.	ICALP	2000	DBLP DOI BibTeX RDF
24	Volker Diekert, Paul Gastin	LTL Is Expressively Complete for Mazurkiewicz Traces.	ICALP	2000	DBLP DOI BibTeX RDF
20	Liang Song, Jianmin Wang 0001, Lijie Wen, Wenxing Wang, Shijie Tan, Hui Kong 0004	Querying Process Models Based on the Temporal Relations between Tasks.	EDOCW	2011	DBLP DOI BibTeX RDF	temporal-order, TPCFP, business process model, retrieval, LTL
20	Ansuman Banerjee	Synthesizability of 3 Party Formal Specifications-Does My Controller See Enough?.	VLSI Design	2010	DBLP DOI BibTeX RDF	Satisfiability, LTL, Realizability, QBF
20	Fuyuan Zhang, Zhengwei Qi, Haibing Guan, Xuezheng Liu, Mao Yang, Zheng Zhang 0001	FiLM: A Runtime Monitoring Tool for Distributed Systems.	SSIRI	2009	DBLP DOI BibTeX RDF	distributed systems, finite automata, runtime monitoring, LTL
20	David A. Cape, Bruce M. McMillin, Benjamin W. Passer, Mayur Thakur	Recursive Decomposition of Progress Graphs.	SSIRI	2009	DBLP DOI BibTeX RDF	dihomotopy, verification, deadlock, SPIN, LTL
20	Joachim Klein 0001, Christel Baier	On-the-Fly Stuttering in the Construction of Deterministic omega -Automata.	CIAA	2007	DBLP DOI BibTeX RDF	Rabin, ?-automaton, determinization, LTL, deterministic, stuttering
20	Mauricio Varea, Bashir M. Al-Hashimi, Luis Alejandro Cortés, Petru Eles, Zebo Peng	Dual Flow Nets: Modeling the control/data-flow relation in embedded systems.	ACM Trans. Embed. Comput. Syst.	2006	DBLP DOI BibTeX RDF	Dual flow nets, tripartite graph, modeling, embedded systems, Petri nets, formal verification, symbolic model checking, CTL, LTL
20	Indranil Saha, Suman Roy 0001	A Finite State Modeling of AFDX Frame Management Using Spin.	FMICS/PDMC	2006	DBLP DOI BibTeX RDF	ARINC, AFDX frame management design, fault tolerance, verification, LTL, Industrial case study, Spin model checker, finite state modeling
20	Karsten Sohr, Michael Drouineaud, Gail-Joon Ahn	Formal specification of role-based security policies for clinical information systems.	SAC	2005	DBLP DOI BibTeX RDF	authorisation constraints, healthcare environments, LTL
20	Koushik Sen, Grigore Rosu, Gul Agha	Runtime safety analysis of multithreaded programs.	ESEC / SIGSOFT FSE	2003	DBLP DOI BibTeX RDF	JMPaX, Java, runtime monitoring, safety analysis, LTL, vector clock, multithreaded program, predictive analysis
20	Ki-Seok Bang, Jin-Young Choi, Chuck Yoo	Comments on 'The Model Checker SPIN'.	IEEE Trans. Software Eng.	2001	DBLP DOI BibTeX RDF	ACSR, model checking, SPIN, process scheduling, LTL
19	Artur Boronat, Reiko Heckel, José Meseguer 0001	Rewriting Logic Semantics and Verification of Model Transformations.	FASE	2009	DBLP DOI BibTeX RDF	Model and graph transformations, LTL model checking, reachability analysis, rewriting logic, MOF, QVT, Maude
19	Jun Sun 0001, Yang Liu 0003, Jin Song Dong, Jing Sun 0002	Compositional encoding for bounded model checking.	Frontiers Comput. Sci. China	2008	DBLP DOI BibTeX RDF	Communication Sequential Processes (CSP), Linear Temporal Logic (LTL), bounded model checking
19	Shobha Vasudevan, E. Allen Emerson, Jacob A. Abraham	Improved verification of hardware designs through antecedent conditioned slicing.	Int. J. Softw. Tools Technol. Transf.	2007	DBLP DOI BibTeX RDF	LTL property, Antecedent conditioned slicing, Verilog RTL, Model checking, Program slicing, Hardware description languages, Hardware verification
19	Twan Basten, Dragan Bosnacki, Marc Geilen	Cluster-Based Partial-Order Reduction.	Autom. Softw. Eng.	2004	DBLP DOI BibTeX RDF	(LTL) model checking, concurrency, formal verification, SPIN, partial-order reduction, state explosion
19	Twan Basten, Dragan Bosnacki	Enhancing Partial-Order Reduction via Process Clustering.	ASE	2001	DBLP DOI BibTeX RDF	(LTL) model checking, concurrency, formal verification, SPIN, partial-order reduction, state explosion
18	Narges Khakpour, Ramtin Khosravi, Marjan Sirjani, Saeed Jalili	Formal analysis of policy-based self-adaptive systems.	SAC	2010	DBLP DOI BibTeX RDF
18	Christine Choppy, Gianna Reggio	A well-founded approach to service modelling with Casl4Soa: part 1 (service in isolation).	SAC	2010	DBLP DOI BibTeX RDF	CASL, UML, SOA, temporal logic
18	Yang Liu 0003, Jun Sun 0001, Jin Song Dong	Scalable Multi-core Model Checking Fairness Enhanced Systems.	ICFEM	2009	DBLP DOI BibTeX RDF
18	Wenhui Zhang	Bounded Semantics of CTL and SAT-Based Verification.	ICFEM	2009	DBLP DOI BibTeX RDF
18	Kari Kähkönen, Jani Lampinen, Keijo Heljanko, Ilkka Niemelä	The LIME Interface Specification Language and Runtime Monitoring Tool.	RV	2009	DBLP DOI BibTeX RDF
18	Alessandro Cimatti, Marco Roveri, Stefano Tonetta	Symbolic Compilation of PSL.	IEEE Trans. Comput. Aided Des. Integr. Circuits Syst.	2008	DBLP DOI BibTeX RDF
18	Matthew Staats, Mats Per Erik Heimdahl	Partial Translation Verification for Untrusted Code-Generators.	ICFEM	2008	DBLP DOI BibTeX RDF
18	Nathalie Bertrand 0001, Patricia Bouyer, Thomas Brihaye, Nicolas Markey	Quantitative Model-Checking of One-Clock Timed Automata under Probabilistic Semantics.	QEST	2008	DBLP DOI BibTeX RDF
18	Marius Kloetzer, Cristian Mahulea, Calin Belta, Laura Recalde, Manuel Silva Suárez	Formal analysis of timed continuous Petri nets.	CDC	2008	DBLP DOI BibTeX RDF
18	Salamah Salamah, Ann Q. Gates	A Technique for Using Model Checkers to Teach Formal Specifications.	CSEE&T	2008	DBLP DOI BibTeX RDF
18	Serge Abiteboul, Luc Segoufin, Victor Vianu	Static analysis of active XML systems.	PODS	2008	DBLP DOI BibTeX RDF	active xml, automatic verification, temporal properties
18	Felicidad Aguado, Pedro Cabalar, Gilberto Pérez 0001, Concepción Vidal	Strongly Equivalent Temporal Logic Programs.	JELIA	2008	DBLP DOI BibTeX RDF
18	Hana Chockler, Arie Gurfinkel, Ofer Strichman	Beyond Vacuity: Towards the Strongest Passing Formula.	FMCAD	2008	DBLP DOI BibTeX RDF
18	Astrid Rakow	Slicing Petri Nets with an Application to Workflow Verification.	SOFSEM	2008	DBLP DOI BibTeX RDF	Net Reduction, Workflow nets, Verification, Slicing, CTL
18	Jinji Yang, Kaile Su, Qingliang Chen	Improving Encoding Efficiency for Bounded Model Checking.	TASE	2008	DBLP DOI BibTeX RDF	encoding, SAT, Bounded Model Checking
18	Sylvain Hallé, Roger Villemaire	Runtime Monitoring of Message-Based Workflows with Data.	EDOC	2008	DBLP DOI BibTeX RDF
18	Salvatore La Torre, Gennaro Parlato	On the Complexity of LtlModel-Checking of Recursive State Machines.	ICALP	2007	DBLP DOI BibTeX RDF
18	Max Goldman, Shmuel Katz	MAVEN: Modular Aspect Verification.	TACAS	2007	DBLP DOI BibTeX RDF
18	Kai Engelhardt, Peter Gammie, Ron van der Meyden	Model Checking Knowledge and Linear Time: PSPACE Cases.	LFCS	2007	DBLP DOI BibTeX RDF
18	Shobha Vasudevan, Vinod Viswanath, Jacob A. Abraham	Efficient Microprocessor Verification using Antecedent Conditioned Slicing.	VLSI Design	2007	DBLP DOI BibTeX RDF
18	Christel Baier, Nathalie Bertrand 0001, Patricia Bouyer, Thomas Brihaye, Marcus Größer	Probabilistic and Topological Semantics for Timed Automata.	FSTTCS	2007	DBLP DOI BibTeX RDF
18	Matthias Schmalz, Hagen Völzer, Daniele Varacca	Model Checking Almost All Paths Can Be Less Expensive Than Checking All Paths.	FSTTCS	2007	DBLP DOI BibTeX RDF
18	Yanyan Xu 0001, Wei Chen 0018, Liang Xu, Wenhui Zhang	Evaluation of SAT-based Bounded Model Checking of ACTL Properties.	TASE	2007	DBLP DOI BibTeX RDF
18	Katsunori Nakamura, Akira Fusaoka	Reasoning About Hybrid Systems Based on a Nonstandard Model.	Australian Conference on Artificial Intelligence	2007	DBLP DOI BibTeX RDF
18	Laura Giordano 0001, Alberto Martelli	Tableau-based automata construction for dynamic linear time temporal logic*.	Ann. Math. Artif. Intell.	2006	DBLP DOI BibTeX RDF	AMS subject classification 03B44, 68N30
18	Laura Bozzelli, Régis Gascon	Branching-Time Temporal Logic Extended with Qualitative Presburger Constraints.	LPAR	2006	DBLP DOI BibTeX RDF
18	Jochen Klose, Tobe Toben, Bernd Westphal, Hartmut Wittke	Check It Out: On the Efficient Formal Verification of Live Sequence Charts.	CAV	2006	DBLP DOI BibTeX RDF
18	Bernhard Möller, Peter Höfner, Georg Struth	Quantales and Temporal Logics.	AMAST	2006	DBLP DOI BibTeX RDF
18	Hong P. Liu, David P. Gluch	Templates and automation for temporal query generation.	ACM Southeast Regional Conference	2006	DBLP DOI BibTeX RDF	architecture analysis & design language, model checking, computation tree logic
18	Sven Schewe	Synthesis for Probabilistic Environments.	ATVA	2006	DBLP DOI BibTeX RDF
18	Thomas Tuerk, Klaus Schneider 0001, Mike Gordon	Model Checking PSL Using HOL and SMV.	Haifa Verification Conference	2006	DBLP DOI BibTeX RDF
18	Eric Bodden, Volker Stolz	Tracechecks: Defining Semantic Interfaces with Temporal Logic.	SC@ETAPS	2006	DBLP DOI BibTeX RDF
18	Ji Zhang, Betty H. C. Cheng	Specifying adaptation semantics.	ACM SIGSOFT Softw. Eng. Notes	2005	DBLP DOI BibTeX RDF	temporal logic, autonomic computing, adaptive software
18	Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha 0001	Concurrent software verification with states, events, and deadlocks.	Formal Aspects Comput.	2005	DBLP DOI BibTeX RDF	Concurrent software, States and events, Counterexample-guided abstraction refinement, Model checking, Temporal logic, Deadlock, Compositional reasoning
18	Hyoung Seok Hong, Hasan Ural	Dependence Testing: Extending Data Flow Testing with Control Dependence.	TestCom	2005	DBLP DOI BibTeX RDF
18	Bernd Finkbeiner, Sven Schewe	Uniform Distributed Synthesis.	LICS	2005	DBLP DOI BibTeX RDF
18	Amir Pnueli	Ranking Abstraction as a Companion to Predicate Abstraction, .	ATVA	2005	DBLP DOI BibTeX RDF
18	Stéphane Demri, David Nowak	Reasoning About Transfinite Sequences.	ATVA	2005	DBLP DOI BibTeX RDF
18	Hana Chockler, Kathi Fisler	Temporal Modalities for Concisely Capturing Timing Diagrams.	CHARME	2005	DBLP DOI BibTeX RDF
18	Shoham Ben-David, Dana Fisman, Sitvanit Ruah	The Safety Simple Subset.	Haifa Verification Conference	2005	DBLP DOI BibTeX RDF
18	Yuhong Zhao 0001, Simon Oberthür, Norma Montealegre, Franz J. Rammig, Martin Kardos	Increasing Dependability by Means of Model-Based Acceptance Test inside RTOS.	PPAM	2005	DBLP DOI BibTeX RDF
18	José Meseguer 0001	Localized Fairness: A Rewriting Semantics.	RTA	2005	DBLP DOI BibTeX RDF
18	Klaus Havelund, Grigore Rosu	Efficient monitoring of safety properties.	Int. J. Softw. Tools Technol. Transf.	2004	DBLP DOI BibTeX RDF	Monitoring, Temporal logics, Safety
18	Mohammad Awedh, Fabio Somenzi	Proving More Properties with Bounded Model Checking.	CAV	2004	DBLP DOI BibTeX RDF
18	John Derrick, Graeme Smith 0001	Linear Temporal Logic and Z Refinement.	AMAST	2004	DBLP DOI BibTeX RDF
18	Kellie Michele Evans	Is Bosco's Rule Universal?	MCU	2004	DBLP DOI BibTeX RDF	gliders, Larger than Life, sliding block memory, spaceships, cellular automata, universal, bugs, register, Game of Life
18	José Meseguer 0001, Grigore Rosu	Rewriting Logic Semantics: From Language Specifications to Formal Analysis Tools.	IJCAR	2004	DBLP DOI BibTeX RDF
18	Sagar Chaki, Edmund M. Clarke, Joël Ouaknine, Natasha Sharygina, Nishant Sinha 0001	State/Event-Based Software Model Checking.	IFM	2004	DBLP DOI BibTeX RDF
18	Laura Giordano 0001, Alberto Martelli	On-the-Fly Automata Construction for Dynamic Linear Time Temporal Logic.	TIME	2004	DBLP DOI BibTeX RDF
18	Edmund M. Clarke, Muralidhar Talupur, Tayssir Touili, Helmut Veith	Verification by Network Decomposition.	CONCUR	2004	DBLP DOI BibTeX RDF
18	Michael Drouineaud, Maksym Bortin, Paolo Torrini, Karsten Sohr	A First Step Towards Formal Verification of Security Policy Properties for RBAC.	QSIC	2004	DBLP DOI BibTeX RDF
18	Beata Sarna-Starosta, C. R. Ramakrishnan 0001	Constraint-Based Model Checking of Data-Independent Systems.	ICFEM	2003	DBLP DOI BibTeX RDF
18	Theo C. Ruys	Optimal Scheduling Using Branch and Bound with SPIN 4.0.	SPIN	2003	DBLP DOI BibTeX RDF
18	Vincent Beaudenon, Emmanuelle Encrenaz, Jean Lou Desbarbieux	Design Validation of ZCSP with SPIN.	ACSD	2003	DBLP DOI BibTeX RDF
18	François Laroussinie, Nicolas Markey, Philippe Schnoebelen	Temporal Logic with Forgettable Past.	LICS	2002	DBLP DOI BibTeX RDF
18	Samik Basu 0001, K. Narayan Kumar, L. Robert Pokorny, C. R. Ramakrishnan 0001	Resource-Constrained Model Checking of Recursive Programs.	TACAS	2002	DBLP DOI BibTeX RDF
18	Rajeev Alur, Kousha Etessami, Salvatore La Torre, Doron A. Peled	Parametric temporal logic for "model measuring".	ACM Trans. Comput. Log.	2001	DBLP DOI BibTeX RDF	model checking, temporal logic, quantitative analysis
18	Klaus Schneider 0001	Improving Automata Generation for Linear Temporal Logic by Considering the Automaton Hierarchy.	LPAR	2001	DBLP DOI BibTeX RDF
18	Rajeev Alur, Kousha Etessami, Mihalis Yannakakis	Realizability and Verification of MSC Graphs.	ICALP	2001	DBLP DOI BibTeX RDF
18	Paritosh K. Pandya	Model Checking CTL*[DC].	TACAS	2001	DBLP DOI BibTeX RDF
18	Moataz Kamel, Stefan Leue	Formalization and Validation of the General Inter-ORB Protocol (GIOP) using PROMELA and SPIN.	Int. J. Softw. Tools Technol. Transf.	2000	DBLP DOI BibTeX RDF	General Inter-ORB Protocol, Promela/Spin, Model checking, Temporal logic, Specification patterns
18	Edmund M. Clarke, Steven M. German, Yuan Lu 0004, Helmut Veith, Dong Wang	Executable Protocol Specification in ESL.	FMCAD	2000	DBLP DOI BibTeX RDF
18	Hubert Comon, Véronique Cortier	Flatness Is Not a Weakness.	CSL	2000	DBLP DOI BibTeX RDF	Counter automata, model-checking, verification, temporal logics, logic in computer science
18	Rance Cleaveland, Gerald Lüttgen	A Semantic Theory for Heterogeneous System Design.	FSTTCS	2000	DBLP DOI BibTeX RDF
18	Amy P. Felty, Frank A. Stomp	Cache Coherency in SCI: Specification and a Sketch of Correctness.	Formal Aspects Comput.	1999	DBLP DOI BibTeX RDF	SCI (Scalable Coherent Interface), Distributed systems, Formal verification, Temporal logic, Cache coherency, IEEE standard
18	Serenella Cerrito, Marta Cialdea Mayer, Sébastien Praud	First Order Linear Temporal Logic over Finite Time Structures.	LPAR	1999	DBLP DOI BibTeX RDF
18	Klaus Schneider 0001, Dirk W. Hoffmann	A HOL Conversion for Translating Linear Time Temporal Logic to omega-Automata.	TPHOLs	1999	DBLP DOI BibTeX RDF
18	Rajeev Alur, Kousha Etessami, Salvatore La Torre, Doron A. Peled	Parametric Temporal Logic for "Model Measuring".	ICALP	1999	DBLP DOI BibTeX RDF
18	Marsha Chechik, Dimitrie O. Paun	Events in Property Patterns.	SPIN	1999	DBLP DOI BibTeX RDF
18	Corina S. Pasareanu, Matthew B. Dwyer, Michael Huth 0001	Assume-Guarantee Model Checking of Software: A Comparative Case Study.	SPIN	1999	DBLP DOI BibTeX RDF
18	Frank Huch	Verification of Erlang Programs using Abstract Interpretation and Model Mhecking.	ICFP	1999	DBLP DOI BibTeX RDF	distributed system, model checking, verification, abstract interpretation, Erlang
18	Armin Biere, Alessandro Cimatti, Edmund M. Clarke, Yunshan Zhu	Symbolic Model Checking without BDDs.	TACAS	1999	DBLP DOI BibTeX RDF
18	Grégoire Sutre, Alain Finkel, Olivier F. Roux, Franck Cassez	Effective Recognizability and Model Checking of Reactive Fiffo Automata.	AMAST	1998	DBLP DOI BibTeX RDF
18	Yonit Kesten, Amir Pnueli, Li-on Raviv	Algorithmic Verification of Linear Temporal Logic Specifications.	ICALP	1998	DBLP DOI BibTeX RDF
18	Sérgio Vale Aguiar Campos, Orna Grumberg	Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System.	CAV	1996	DBLP DOI BibTeX RDF
18	Jan Paredis	Coevolutionary Life-Time Learning.	PPSN	1996	DBLP DOI BibTeX RDF
18	Doron A. Peled, Thomas Wilke, Pierre Wolper	An Algorithmic Approach for Checking Closure Properties of omega-Regular Languages.	CONCUR	1996	DBLP DOI BibTeX RDF
18	Mahesh Girkar, Robert Moll	New Results on the Analysis of Concurrent Systems with an Infinite Number of Processes.	CONCUR	1994	DBLP DOI BibTeX RDF
15	Mojtaba Valizadeh, Nathanaël Fijalkow, Martin Berger 0001	LTL learning on GPUs.	CoRR	2024	DBLP DOI BibTeX RDF
15	Jiming Ren, Haris Miller, Karen M. Feigh, Samuel Coogan 0001, Ye Zhao 0002	LTL-D*: Incrementally Optimal Replanning for Feasible and Infeasible Tasks in Linear Temporal Logic Specifications.	CoRR	2024	DBLP DOI BibTeX RDF
15	Luca Geatti, Alessio Mansutti, Angelo Montanari	Succinctness of Cosafety Fragments of LTL via Combinatorial Proof Systems (extended version).	CoRR	2024	DBLP DOI BibTeX RDF