Hits ?▲ |
Authors |
Title |
Venue |
Year |
Link |
Author keywords |
33 | Kais Klai, Denis Poitrenaud |
MC-SOG: An LTL Model Checker Based on Symbolic Observation Graphs. |
Petri Nets |
2008 |
DBLP DOI BibTeX RDF |
|
33 | Jiri Barnat, Lubos Brim, Pavel Simecek, M. Weber |
Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking. |
TACAS |
2008 |
DBLP DOI BibTeX RDF |
|
33 | Jiri Barnat, Lubos Brim, Petr Rockai |
Scalable Multi-core LTL Model-Checking. |
SPIN |
2007 |
DBLP DOI BibTeX RDF |
|
33 | Juan Antonio Navarro Pérez, Andrei Voronkov |
Encodings of Bounded LTL Model Checking in Effectively Propositional Logic. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
33 | Stéphane Demri, Régis Gascon |
The Effects of Bounding Syntactic Resources on Presburger LTL. |
TIME |
2007 |
DBLP DOI BibTeX RDF |
|
33 | Mohammed Al Achhab, Ahmed Hammad, Hassan Mountassir |
Verifying LTL Properties on Hierarchical Systems: Application to Aircraft Autopilot. |
ISoLA |
2006 |
DBLP DOI BibTeX RDF |
|
33 | Alexandre Genon, Thierry Massart, Cédric Meuter |
Monitoring Distributed Controllers: When an Efficient LTL Algorithm on Sequences Is Needed to Model-Check Traces. |
FM |
2006 |
DBLP DOI BibTeX RDF |
testing of asynchronous distributed systems, global properties, model checking of traces, monitor |
33 | Wenhui Zhang |
SAT-Based Verification of LTL Formulas. |
FMICS/PDMC |
2006 |
DBLP DOI BibTeX RDF |
|
33 | Barbara Jobstmann, Roderick Bloem |
Optimizations for LTL Synthesis. |
FMCAD |
2006 |
DBLP DOI BibTeX RDF |
|
33 | Roberto Sebastiani, Stefano Tonetta, Moshe Y. Vardi |
Symbolic Systems, Explicit Properties: On Hybrid Approaches for LTL Symbolic Model Checking. |
CAV |
2005 |
DBLP DOI BibTeX RDF |
|
33 | Radek Pelánek, Jan Strejcek |
Deeper Connections Between LTL and Alternating Automata. |
CIAA |
2005 |
DBLP DOI BibTeX RDF |
|
33 | Jiri Barnat, Lubos Brim, Ivana Cerná |
Cluster-Based LTL Model Checking of Large Systems. |
FMCO |
2005 |
DBLP DOI BibTeX RDF |
|
33 | Timo Latvala, Marko Mäkelä |
LTL Model Checking for Modular Petri Nets. |
ICATPN |
2004 |
DBLP DOI BibTeX RDF |
|
33 | Fang Wang, Sofiène Tahar, Otmane Aït Mohamed |
First-Order LTL Model Checking Using MDGs. |
ATVA |
2004 |
DBLP DOI BibTeX RDF |
|
33 | Paul Gastin, Madhavan Mukund, K. Narayan Kumar |
Local LTL with Past Constants Is Expressively Complete for Mazurkiewicz Traces. |
MFCS |
2003 |
DBLP DOI BibTeX RDF |
concurrency, Temporal logics, Mazurkiewicz traces |
33 | Roberto Sebastiani, Stefano Tonetta |
"More Deterministic" vs. "Smaller" Büchi Automata for Efficient LTL Model Checking. |
CHARME |
2003 |
DBLP DOI BibTeX RDF |
|
33 | Jiri Barnat, Lubos Brim, Jakub Chaloupka |
Parallel Breadth-First Search LTL Model-Checking. |
ASE |
2003 |
DBLP DOI BibTeX RDF |
|
33 | Alessandro Cimatti, Marco Pistore, Marco Roveri, Roberto Sebastiani |
Improving the Encoding of LTL Model Checking into SAT. |
VMCAI |
2002 |
DBLP DOI BibTeX RDF |
|
33 | Paul Gastin, Denis Oddoux |
Fast LTL to Büchi Automata Translation. |
CAV |
2001 |
DBLP DOI BibTeX RDF |
|
33 | Michael Leuschel, Thierry Massart, Andrew Currie |
How to Make FDR Spin LTL Model Checking of CSP by Refinement. |
FME |
2001 |
DBLP DOI BibTeX RDF |
|
33 | Javier Esparza, Keijo Heljanko |
Implementing LTL Model Checking with Net Unfoldings. |
SPIN |
2001 |
DBLP DOI BibTeX RDF |
|
33 | Javier Esparza, Claus Schröter |
Net Reductions for LTL Model-Checking. |
CHARME |
2001 |
DBLP DOI BibTeX RDF |
|
33 | Klaus Schneider 0001 |
Yet another Look at the LTL Model Checking. |
CHARME |
1999 |
DBLP DOI BibTeX RDF |
|
33 | Javier Esparza, Stephan Melzer |
Model Checking LTL Using Constraint Programming. |
ICATPN |
1997 |
DBLP DOI BibTeX RDF |
|
30 | Alessandro Artale, Luca Geatti, Nicola Gigante, Andrea Mazzullo, Angelo Montanari |
LTL over Finite Words Can Be Exponentially More Succinct Than Pure-Past LTL, and vice versa. |
TIME |
2023 |
DBLP DOI BibTeX RDF |
|
30 | Alessandro Artale, Luca Geatti, Nicola Gigante, Andrea Mazzullo, Angelo Montanari |
A Singly Exponential Transformation of LTL[X, F] into Pure Past LTL. |
KR |
2023 |
DBLP DOI BibTeX RDF |
|
30 | Jan Kretínský, Tobias Meggendorfer, Salomon Sickert |
LTL Store: Repository of LTL formulae from literature and case studies. |
CoRR |
2018 |
DBLP BibTeX RDF |
|
30 | Ala-Eddine Ben Salem |
Improving the model checking of stutter-invariant LTL properties. (Amélioration du model checking des propriétés LTL insensibles au bégaiement). |
|
2014 |
RDF |
|
30 | Michaël Guedj |
BSP Algorithms for LTL & CTL* Model Checking of Security Protocols. (Algorithmes BSP pour la vérification de modèles LTL et CTL* pour les protocoles de sécurité). |
|
2012 |
RDF |
|
30 | Vineet Kahlon, Aarti Gupta |
On the analysis of interacting pushdown systems. |
POPL |
2007 |
DBLP DOI BibTeX RDF |
model checking, concurrency, dataflow analysis, LTL, mu-calculus, pushdown systems |
30 | Benoît Combemale, Xavier Crégut, Pierre-Loïc Garoche, Xavier Thirioux, François Vernadat 0001 |
A Property-Driven Approach to Formal Verification of Process Models. |
ICEIS (Selected Papers) |
2007 |
DBLP DOI BibTeX RDF |
Properties Validation, Temporal OCL, Models Semantics, Verification, Petri Nets, Process Model, Model Transformation, Metamodelling, LTL |
30 | Chao Wang 0001, Roderick Bloem, Gary D. Hachtel, Kavita Ravi, Fabio Somenzi |
Compositional SCC Analysis for Language Emptiness. |
Formal Methods Syst. Des. |
2006 |
DBLP DOI BibTeX RDF |
language emptiness, model checking, BDD, LTL, abstraction refinement |
30 | Xi Chen 0024, Harry Hsieh, Felice Balarin |
Verification Approach of Metropolis Design Framework for Embedded Systems. |
Int. J. Parallel Program. |
2006 |
DBLP DOI BibTeX RDF |
metropolis, simulation, formal verification, meta-model, spin, LTL, property, LOC |
29 | Malay K. Ganai, Aarti Gupta |
Efficient BMC for Multi-Clock Systems with Clocked Specifications. |
ASP-DAC |
2007 |
DBLP DOI BibTeX RDF |
OpenCores multiclock system benchmarks, clocked specifications, multiphased clocks, level-sensitive latches, SAT-based bounded model checking, synchronous multiclock systems, clocked LTL properties, clock modeling schemes, clock constraints, loop-checks, gated clocks |
29 | Kimmo Varpaaniemi |
On Stubborn Sets in the Verification of Linear Time Temporal Properties. |
Formal Methods Syst. Des. |
2005 |
DBLP DOI BibTeX RDF |
reduced state space generation, stubborn sets, verification of LTL formulas, reachability analysis |
28 | Astrid Rakow |
Decompositional Petri Net Reductions. |
IFM |
2009 |
DBLP DOI BibTeX RDF |
|
28 | Thomas Noll 0001, Stefan Rieger |
Verifying Dynamic Pointer-Manipulating Threads. |
FM |
2008 |
DBLP DOI BibTeX RDF |
|
28 | Amir Pnueli, Aleksandr Zaks |
On the Merits of Temporal Testers. |
25 Years of Model Checking |
2008 |
DBLP DOI BibTeX RDF |
|
28 | Yogendra Narain Singh, Phalguni Gupta |
Quantitative Evaluation of Normalization Techniques of Matching Scores in Multimodal Biometric Systems. |
ICB |
2007 |
DBLP DOI BibTeX RDF |
|
28 | Wenhui Zhang |
Model Checking with SAT-Based Characterization of ACTL Formulas. |
ICFEM |
2007 |
DBLP DOI BibTeX RDF |
|
28 | Martin Leucker, César Sánchez 0001 |
Regular Linear Temporal Logic. |
ICTAC |
2007 |
DBLP DOI BibTeX RDF |
|
28 | Sven Schewe, Bernd Finkbeiner |
Bounded Synthesis. |
ATVA |
2007 |
DBLP DOI BibTeX RDF |
|
28 | Michael Bauland, Thomas Schneider 0002, Henning Schnoor, Ilka Schnoor, Heribert Vollmer |
The Complexity of Generalized Satisfiability for Linear Temporal Logic. |
FoSSaCS |
2007 |
DBLP DOI BibTeX RDF |
computational complexity, linear temporal logic |
28 | Andreas Bauer 0002, Martin Leucker, Christian Schallhart |
The Good, the Bad, and the Ugly, But How Ugly Is Ugly? |
RV |
2007 |
DBLP DOI BibTeX RDF |
|
28 | Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli |
Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems. |
CADE |
2007 |
DBLP DOI BibTeX RDF |
|
28 | Conghua Zhou |
A compositional symbolic verification framework for concurrent software. |
Infoscale |
2007 |
DBLP DOI BibTeX RDF |
model checking, composition, abstract, SAT |
28 | Matteo Dell'Amico, Maura Cerioli |
DO-Casl: An Observer-Based Casl Extension for Dynamic Specifications. |
AMAST |
2006 |
DBLP DOI BibTeX RDF |
|
28 | Orna Kupferman, Robby Lampert |
On the Construction of Fine Automata for Safety Properties. |
ATVA |
2006 |
DBLP DOI BibTeX RDF |
|
28 | Alessandro Cimatti, Marco Roveri, Simone Semprini, Stefano Tonetta |
From PSL to NBA: a Modular Symbolic Encoding. |
FMCAD |
2006 |
DBLP DOI BibTeX RDF |
|
28 | Christian Dax, Martin Hofmann 0001, Martin Lange |
A Proof System for the Linear Time µ-Calculus. |
FSTTCS |
2006 |
DBLP DOI BibTeX RDF |
|
28 | Syed Suhaib, Deepak Mathaikutty, Sandeep K. Shukla, David Berner |
XFM: An incremental methodology for developing formal models. |
ACM Trans. Design Autom. Electr. Syst. |
2005 |
DBLP DOI BibTeX RDF |
Extreme formal modeling, prescriptive formal models, property ordering, property refactoring, formal specification, formal verification, extreme programming, SPIN, SMV |
28 | Ansuman Banerjee, Pallab Dasgupta |
The open family of temporal logics: Annotating temporal operators with input constraints. |
ACM Trans. Design Autom. Electr. Syst. |
2005 |
DBLP DOI BibTeX RDF |
|
28 | Wil M. P. van der Aalst, H. T. de Beer, Boudewijn F. van Dongen |
Process Mining and Verification of Properties: An Approach Based on Temporal Logic. |
OTM Conferences (1) |
2005 |
DBLP DOI BibTeX RDF |
data mining, Petri nets, temporal logic, workflow management, business process management, Process mining |
28 | Doron Bustan, Alon Flaisher, Orna Grumberg, Orna Kupferman, Moshe Y. Vardi |
Regular Vacuity. |
CHARME |
2005 |
DBLP DOI BibTeX RDF |
|
28 | Stéphane Demri, Régis Gascon |
Verification of Qualitative Constraints. |
CONCUR |
2005 |
DBLP DOI BibTeX RDF |
|
28 | Rajeev Alur, Kousha Etessami, P. Madhusudan |
A Temporal Logic of Nested Calls and Returns. |
TACAS |
2004 |
DBLP DOI BibTeX RDF |
|
28 | Salvatore La Torre, Margherita Napoli, Mimmo Parente, Gennaro Parlato |
Hierarchical and Recursive State Machines with Context-Dependent Properties. |
ICALP |
2003 |
DBLP DOI BibTeX RDF |
Model Checking, Temporal Logic, Automata |
28 | Timo Latvala |
Efficient Model Checking of Safety Properties. |
SPIN |
2003 |
DBLP DOI BibTeX RDF |
|
28 | Koushik Sen, Grigore Rosu, Gul Agha |
Generating Optimal Linear Temporal Logic Monitors by Coinduction. |
ASIAN |
2003 |
DBLP DOI BibTeX RDF |
|
28 | Bozena Wozna, Andrzej Zbrzezny |
Checking ACTL* Properties of Discrete Timed Automata via Bounded Model Checking. |
FORMATS |
2003 |
DBLP DOI BibTeX RDF |
|
28 | Orna Kupferman, Nir Piterman, Moshe Y. Vardi |
Model Checking Linear Properties of Prefix-Recognizable Systems. |
CAV |
2002 |
DBLP DOI BibTeX RDF |
|
28 | Klaus Havelund, Grigore Rosu |
Synthesizing Monitors for Safety Properties. |
TACAS |
2002 |
DBLP DOI BibTeX RDF |
|
28 | Moshe Y. Vardi |
Branching vs. Linear Time: Final Showdown. |
TACAS |
2001 |
DBLP DOI BibTeX RDF |
|
28 | Thomas A. Henzinger, Rupak Majumdar |
Symbolic Model Checking for Rectangular Hybrid Systems. |
TACAS |
2000 |
DBLP DOI BibTeX RDF |
|
28 | Françoise Bellegarde, Jacques Julliand, Olga Kouchnarenko |
Ready-Simulation Is Not Ready to Express a Modular Refinement Relation. |
FASE |
2000 |
DBLP DOI BibTeX RDF |
|
28 | Thomas A. Henzinger, Benjamin Horowitz, Rupak Majumdar |
Rectangular Hybrid Games. |
CONCUR |
1999 |
DBLP DOI BibTeX RDF |
|
28 | Orna Kupferman, Moshe Y. Vardi |
Modular Model Checking. |
COMPOS |
1997 |
DBLP DOI BibTeX RDF |
|
28 | Ahmed Bouajjani, Peter Habermehl |
Constrained Properties, Semilinear Systems, and Petri Nets. |
CONCUR |
1996 |
DBLP DOI BibTeX RDF |
|
28 | Bengt Jonsson 0001, Yih-Kuen Tsay |
Assumption/Guarantee Specifications in Linear-Time Temporal Logic (Extended Abstract). |
TAPSOFT |
1995 |
DBLP DOI BibTeX RDF |
|
24 | Lars Kuhtz, Bernd Finkbeiner |
LTL Path Checking Is Efficiently Parallelizable. |
ICALP (2) |
2009 |
DBLP DOI BibTeX RDF |
|
24 | Erion Plaku, Lydia E. Kavraki, Moshe Y. Vardi |
Falsification of LTL Safety Properties in Hybrid Systems. |
TACAS |
2009 |
DBLP DOI BibTeX RDF |
|
24 | Matthias Schmalz, Daniele Varacca, Hagen Völzer |
Counterexamples in Probabilistic LTL Model Checking for Markov Chains. |
CONCUR |
2009 |
DBLP DOI BibTeX RDF |
|
24 | Jiri Barnat, Lubos Brim, Petr Rockai |
DiVinE Multi-Core - A Parallel LTL Model-Checker. |
ATVA |
2008 |
DBLP DOI BibTeX RDF |
|
24 | Guangquan Zhang 0002, Rong Mei |
An Approach of Concurrent Object-Oriented Program Slicing Based on LTL Property. |
CSSE (2) |
2008 |
DBLP DOI BibTeX RDF |
|
24 | Gordon Fraser 0001, Paul Ammann |
Reachability and Propagation for LTL Requirements Testing. |
QSIC |
2008 |
DBLP DOI BibTeX RDF |
requirements testing, software testing, automated testing, test case generation, property testing |
24 | Salamah Salamah, Ann Q. Gates, Vladik Kreinovich, Steve Roach |
Verification of Automatically Generated Pattern-Based LTL Specifications. |
HASE |
2007 |
DBLP DOI BibTeX RDF |
|
24 | Alessandro Armando, Roberto Carbone, Luca Compagna |
LTL Model Checking for Security Protocols. |
CSF |
2007 |
DBLP DOI BibTeX RDF |
|
24 | Kais Klai, Laure Petrucci, Michel A. Reniers |
An Incremental and Modular Technique for Checking LTL\X Properties of Petri Nets. |
FORTE |
2007 |
DBLP DOI BibTeX RDF |
|
24 | Jocelyn Simmonds, Jessica Davies 0001, Arie Gurfinkel, Marsha Chechik |
Exploiting Resolution Proofs to Speed Up LTL Vacuity Detection for BMC. |
FMCAD |
2007 |
DBLP DOI BibTeX RDF |
|
24 | Muffy Calder, Alice Miller 0001 |
Feature interaction detection by pairwise analysis of LTL properties - A case study. |
Formal Methods Syst. Des. |
2006 |
DBLP DOI BibTeX RDF |
Distributed systems, Model checking, Feature interaction, Communicating processes, Communications services |
24 | Jaco Geldenhuys, Henri Hansen |
Larger Automata and Less Work for LTL Model Checking. |
SPIN |
2006 |
DBLP DOI BibTeX RDF |
|
24 | Stefan Edelkamp, Shahid Jabbar |
Large-Scale Directed Model Checking LTL. |
SPIN |
2006 |
DBLP DOI BibTeX RDF |
|
24 | Marius Kloetzer, Calin Belta |
A Fully Automated Framework for Control of Linear Systems from LTL Specifications. |
HSCC |
2006 |
DBLP DOI BibTeX RDF |
|
24 | Peter Niebert, Doron A. Peled |
Efficient Model Checking for LTL with Partial Order Snapshots. |
TACAS |
2006 |
DBLP DOI BibTeX RDF |
|
24 | Werner Damm, Guilherme Pinto, Stefan Ratschan |
Guaranteed Termination in the Verification of LTL Properties of Non-linear Robust Discrete Time Hybrid Systems. |
ATVA |
2005 |
DBLP DOI BibTeX RDF |
|
24 | Aidan Harding, Mark Ryan 0001, Pierre-Yves Schobbens |
A New Algorithm for Strategy Synthesis in LTL Games. |
TACAS |
2005 |
DBLP DOI BibTeX RDF |
|
24 | Claus Schröter, Victor Khomenko |
Parallel LTL-X Model Checking of High-Level Petri Nets Based on Unfoldings. |
CAV |
2004 |
DBLP DOI BibTeX RDF |
|
24 | YoungMin Kwon, Gul Agha |
Linear Inequality LTL (iLTL): A Model Checker for Discrete Time Markov Chains. |
ICFEM |
2004 |
DBLP DOI BibTeX RDF |
|
24 | Anca Muscholl, Igor Walukiewicz |
An NP-Complete Fragment of LTL. |
Developments in Language Theory |
2004 |
DBLP DOI BibTeX RDF |
|
24 | Jaco Geldenhuys, Antti Valmari |
Tarjan's Algorithm Makes On-the-Fly LTL Verification More Efficient. |
TACAS |
2004 |
DBLP DOI BibTeX RDF |
|
24 | Lubos Brim, Ivana Cerná, Pavel Moravec 0002, Jirí Simsa |
Accepting Predecessors Are Better than Back Edges in Distributed LTL Model-Checking. |
FMCAD |
2004 |
DBLP DOI BibTeX RDF |
|
24 | Amir Pnueli, Tamarah Arons |
TLPVS: A PVS-Based LTL Verification System. |
Verification: Theory and Practice |
2003 |
DBLP DOI BibTeX RDF |
|
24 | Paul Gastin, Denis Oddoux |
LTL with Past and Two-Way Very-Weak Alternating Automata. |
MFCS |
2003 |
DBLP DOI BibTeX RDF |
|
24 | Daniel Große, Rolf Drechsler |
Formal verification of LTL formulas for SystemC designs. |
ISCAS (5) |
2003 |
DBLP DOI BibTeX RDF |
|
24 | Aidan Harding, Mark Ryan 0001, Pierre-Yves Schobbens |
Towards Symbolic Strategy Synthesis for \left\langle {\left\langle A \right\rangle } \right\rangle-LTL. |
TIME |
2003 |
DBLP DOI BibTeX RDF |
|
24 | Dimitra Giannakopoulou, Flavio Lerda |
From States to Transitions: Improving Translation of LTL Formulae to Büchi Automata. |
FORTE |
2002 |
DBLP DOI BibTeX RDF |
|
24 | Stéphane Demri, Deepak D'Souza |
An Automata-Theoretic Approach to Constraint LTL. |
FSTTCS |
2002 |
DBLP DOI BibTeX RDF |
|
24 | Lubos Brim, Ivana Cerná, Martin Necesal |
Randomization Helps in LTL Model Checking. |
PAPM-PROBMIV |
2001 |
DBLP DOI BibTeX RDF |
|
24 | Jiri Barnat, Lubos Brim, Jitka Stríbrná |
Distributed LTL Model-Checking in SPIN. |
SPIN |
2001 |
DBLP DOI BibTeX RDF |
|
24 | Javier Esparza, Antonín Kucera 0001, Stefan Schwoon |
Model-Checking LTL with Regular Valuations for Pushdown Systems. |
TACS |
2001 |
DBLP DOI BibTeX RDF |
|