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 |
|