Search results for "Infinite state systems"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
3	Tobias Schüle, Klaus Schneider	Bounded model checking of infinite state systems.	Formal Methods in System Design	2007	DBLP DOI BibTeX RDF	Temporal logic hierarchy, Global model checking, Local model checking, Bounded model checking, Infinite state systems
3	Thomas Mailund	Analysing Infinite-State Systems by Combining Equivalence Reduction and the Sweep-Line Method.	ICATPN	2002	DBLP DOI BibTeX RDF	Timed Coloured Petri Nets, Infinite-State Systems, State Space Analysis, Reduction Techniques
3	Parosh Aziz Abdulla, Aletta Nylén	Better is Better than Well: On Efficient Verification of Infinite-State Systems.	LICS	2000	DBLP DOI BibTeX RDF	lossy channel systems, integral relational automata, model checking, Verification, timed Petri nets, infinite-state systems, broadcast protocols
2	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
2	Nikola Bogunovi, Edgar Pek	Model Checking Procedures for Infinite State Systems.	ECBS	2006	DBLP DOI BibTeX RDF
2	Matteo Slanina, Henny B. Sipma, Zohar Manna	Proving ATL* Properties of Infinite-State Systems.	ICTAC	2006	DBLP DOI BibTeX RDF
2	Randal E. Bryant	Formal Verification of Infinite State Systems Using Boolean Methods.	LICS	2006	DBLP DOI BibTeX RDF
2	Jesse D. Bingham, Alan J. Hu	Empirically Efficient Verification for a Class of Infinite-State Systems.	TACAS	2005	DBLP DOI BibTeX RDF
2	Lee Pike, Steven D. Johnson	The formal verification of a reintegration protocol.	EMSOFT	2005	DBLP DOI BibTeX RDF	infinite-state bounded model-checking, reintegration protocol, real-time, formal verification, infinite-state systems
2	Abhay Vardhan, Mahesh Viswanathan	Learning to verify branching time properties.	ASE	2005	DBLP DOI BibTeX RDF	CTL, computational learning theory, infinite state systems
2	Sébastien Bardin, Alain Finkel, Jérôme Leroux, Ph. Schnoebelen	Flat Acceleration in Symbolic Model Checking.	ATVA	2005	DBLP DOI BibTeX RDF	verification of infinite-state systems, acceleration, symbolic model checking
2	Antonín Kucera, Ph. Schnoebelen	A General Approach to Comparing Infinite-State Systems with Their Finite-State Specifications.	CONCUR	2004	DBLP DOI BibTeX RDF
2	Tobias Schüle, Klaus Schneider	Global vs. Local Model Checking: A Comparison of Verification Techniques for Infinite State Systems.	SEFM	2004	DBLP DOI BibTeX RDF
2	Tobias Schüle, Klaus Schneider	Bounded model checking of infinite state systems: exploiting the automata hierarchy.	MEMOCODE	2004	DBLP DOI BibTeX RDF
2	Oscar H. Ibarra	Automata-Theoretic Techniques for Analyzing Infinite-State Systems.	CIAA	2004	DBLP DOI BibTeX RDF
2	Carron Shankland, Jeremy Bryans, Lionel Morel	Expressing Iterative Properties Logically in a Symbolic Setting.	AMAST	2004	DBLP DOI BibTeX RDF	formal verification, temporal logics, LOTOS, infinite state systems, symbolic representation
2	Parosh Aziz Abdulla, S. Purushothaman Iyer, Aletta Nylén	SAT-Solving the Coverability Problem for Petri Nets.	Formal Methods in System Design	2004	DBLP DOI BibTeX RDF	Petri nets, unfoldings, coverability, infinite state systems, partial-order methods
2	Giorgio Delzanno, Jean-François Raskin, Laurent Van Begin	Covering sharing trees: a compact data structure for parameterized verification.	STTT	2004	DBLP DOI BibTeX RDF	Efficient data structures, Heuristics, Static analysis, Constraints, Symbolic model checking, Infinite-state systems
2	Gaoyan Xie, Zhe Dang, Oscar H. Ibarra	A Solvable Class of Quadratic Diophantine Equations with Applications to Verification of Infinite-State Systems.	ICALP	2003	DBLP DOI BibTeX RDF
2	Giorgio Delzanno, Maurizio Gabbrielli, Maria Chiara Meo	Compositional Verification of Infinite State Systems.	ICLP	2003	DBLP DOI BibTeX RDF
2	Tatiana Rybina, Andrei Voronkov	A Logical Reconstruction of Reachability.	Ershov Memorial Conference	2003	DBLP DOI BibTeX RDF	reachability analysis, infinite-state systems, model theory, theoretical foundations
2	Jan Friso Groote, Tim A. C. Willemse	A Checker for Modal Formulae for Processes with Data.	FMCO	2003	DBLP DOI BibTeX RDF	First Order Modal -Calculus, First Order Boolean Equation Systems, Data-Dependent Systems, Model Checking, Infinite State Systems, CRL
2	Antonín Kucera, Petr Jancar	Equivalence-Checking with Infinite-State Systems: Techniques and Results.	SOFSEM	2002	DBLP DOI BibTeX RDF
2	Alain Finkel, Jérôme Leroux	How to Compose Presburger-Accelerations: Applications to Broadcast Protocols.	FSTTCS	2002	DBLP DOI BibTeX RDF	Presburger model checking, verification, acceleration, infinite-state systems, reachability set
2	Werner Damm, Bengt Jonsson	Eliminating Queues from RT UML Model Representations.	FTRTFT	2002	DBLP DOI BibTeX RDF	RT UML, verification of infinite state systems, protocol verification, Real-time distributed systems
2	Antonín Kucera, Richard Mayr	Weak Bisimilarity with Infinite-State Systems Can Be Decided in Polynomial Time.	CONCUR	1999	DBLP DOI BibTeX RDF
2	Witold Charatonik, Andreas Podelski	Set-Based Analysis of Reactive Infinite-State Systems.	TACAS	1998	DBLP DOI BibTeX RDF
2	Saddek Bensalem, Yassine Lakhnech, Sam Owre	Computing Abstractions of Infinite State Systems Compositionally and Automatically.	CAV	1998	DBLP DOI BibTeX RDF
1	Daniele Zucchelli, Enrica Nicolini	A Decidability Result for the Model Checking of Infinite-State Systems.	J. Autom. Reasoning	2012	DBLP DOI BibTeX RDF
1	Fang Yu, Chao Wang (eds.)	Proceedings 13th International Workshop on Verification of Infinite-State Systems	INFINITY	2011	DBLP DOI BibTeX RDF
1	Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Valerio Senni	Generalization Strategies for the Verification of Infinite State Systems	CoRR	2011	DBLP BibTeX RDF
1	Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Valerio Senni	Improving Reachability Analysis of Infinite State Systems by Specialization.	RP	2011	DBLP DOI BibTeX RDF
1	Doron Peled, Sven Schewe	Practical Distributed Control Synthesis	INFINITY	2011	DBLP DOI BibTeX RDF
1	Alberto Ciaffaglione	A coinductive semantics of the Unlimited Register Machine	INFINITY	2011	DBLP DOI BibTeX RDF
1	Laurent Fribourg, Bertrand Revol, Romain Soulat	Synthesis of Switching Rules for Ensuring Reachability Properties of Sampled Linear Systems	INFINITY	2011	DBLP DOI BibTeX RDF
1	Christian Krause, Holger Giese	Model Checking Probabilistic Real-Time Properties for Service-Oriented Systems with Service Level Agreements	INFINITY	2011	DBLP DOI BibTeX RDF
1	Alex Spelten, Wolfgang Thomas, Sarah Winter	Trees over Infinite Structures and Path Logics with Synchronization	INFINITY	2011	DBLP DOI BibTeX RDF
1	Takashi Tomita, Shigeki Hagihara, Naoki Yonezaki	A Probabilistic Temporal Logic with Frequency Operators and Its Model Checking	INFINITY	2011	DBLP DOI BibTeX RDF
1	Yu-Fang Chen, Ahmed Rezine (eds.)	Proceedings 12th International Workshop on Verification of Infinite-State Systems	INFINITY	2010	DBLP DOI BibTeX RDF
1	Orna Kupferman, Nir Piterman, Moshe Y. Vardi	An Automata-Theoretic Approach to Infinite-State Systems.	Essays in Memory of Amir Pnueli	2010	DBLP DOI BibTeX RDF
1	Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Valerio Senni	Program Specialization for Verifying Infinite State Systems: An Experimental Evaluation.	LOPSTR	2010	DBLP DOI BibTeX RDF
1	Hanifa Boucheneb, Kamel Barkaoui	On interleaving in {P,A}-Time Petri nets with strong semantics	INFINITY	2010	DBLP DOI BibTeX RDF
1	Stéphane Demri	On Selective Unboundedness of VASS	INFINITY	2010	DBLP DOI BibTeX RDF
1	Étienne André	IMITATOR II: A Tool for Solving the Good Parameters Problem in Timed Automata	INFINITY	2010	DBLP DOI BibTeX RDF
1	Frédéric Peschanski, Hanna Klaudel, Raymond R. Devillers	A Decidable Characterization of a Graphical Pi-calculus with Iterators	INFINITY	2010	DBLP DOI BibTeX RDF
1	Oded Maler, Kim G. Larsen, Bruce H. Krogh	On Zone-Based Analysis of Duration Probabilistic Automata	INFINITY	2010	DBLP DOI BibTeX RDF
1	Bernard Boigelot, Julien Brusten, Jean-François Degbomont	Implicit Real Vector Automata	INFINITY	2010	DBLP DOI BibTeX RDF
1	Nathalie Bertrand, Christophe Morvan	Probabilistic regular graphs	INFINITY	2010	DBLP DOI BibTeX RDF
1	Mohamed Faouzi Atig, Ahmed Bouajjani, Sebastian Burckhardt, Madanlal Musuvathi	On the verification problem for weak memory models.	POPL	2010	DBLP DOI BibTeX RDF	lossy channel systems, program verification, infinite state systems, relaxed memory models
1	Axel Legay (eds.)	Proceedings International Workshop on Verification of Infinite-State Systems	INFINITY	2009	DBLP DOI BibTeX RDF
1	Laurent Fribourg, Étienne André	An Inverse Method for Policy-Iteration Based Algorithms	INFINITY	2009	DBLP DOI BibTeX RDF
1	Nguyen Van Tang	A Tighter Bound for the Determinization of Visibly Pushdown Automata	INFINITY	2009	DBLP DOI BibTeX RDF
1	Christophe Morvan	On external presentations of infinite graphs	INFINITY	2009	DBLP DOI BibTeX RDF
1	Florent Bouchy, Alain Finkel, Pierluigi San Pietro	Dense-choice Counter Machines revisited	INFINITY	2009	DBLP DOI BibTeX RDF
1	Bahareh Badban, Stefan Leue, Jan-Georg Smaus	Automated Predicate Abstraction for Real-Time Models	INFINITY	2009	DBLP DOI BibTeX RDF
1	Parosh Aziz Abdulla	Infinite-State Verification: From Transition Systems to Markov Chains.	QEST	2009	DBLP DOI BibTeX RDF	Model Checking, Markov Chains, Program Verification, Infinite-State Systems
1	Daniel Klink, Anne Remke, Boudewijn R. Haverkort, Joost-Pieter Katoen	Time-Bounded Reachability in Tree-Structured QBDs by Abstraction.	QEST	2009	DBLP DOI BibTeX RDF	Applications, Abstraction, Probabilistic model checking, Infinite-state systems
1	Alin Deutsch, Richard Hull, Fabio Patrizi, Victor Vianu	Automatic verification of data-centric business processes.	ICDT	2009	DBLP DOI BibTeX RDF
1	Hongfei Fu	Branching Bisimilarity between Finite-State Systems and BPA or Normed BPP Is Polynomial-Time Decidable.	APLAS	2009	DBLP DOI BibTeX RDF
1	Christoph Haase, Stephan Kreutzer, Joël Ouaknine, James Worrell	Reachability in Succinct and Parametric One-Counter Automata.	CONCUR	2009	DBLP DOI BibTeX RDF
1	Wolfgang Thomas	The Reachability Problem over Infinite Graphs.	CSR	2009	DBLP DOI BibTeX RDF
1	Kenneth L. McMillan, Lenore D. Zuck	Abstract Counterexamples for Non-disjunctive Abstractions.	RP	2009	DBLP DOI BibTeX RDF
1	Silvio Ghilardi, Silvio Ranise	Goal-Directed Invariant Synthesis for Model Checking Modulo Theories.	TABLEAUX	2009	DBLP DOI BibTeX RDF
1	Laura Bozzelli, Mojmír Kretínský, Vojtech Rehák, Jan Strejcek	On decidability of LTL model checking for process rewrite systems.	Acta Inf.	2009	DBLP DOI BibTeX RDF
1	Michael Fisher, Boris Konev, Alexei Lisitsa	Temporal Verification of Fault-Tolerant Protocols.	Methods, Models and Tools for Fault Tolerance	2009	DBLP DOI BibTeX RDF
1	Jochen Eisinger, Felix Klaedtke	Don't care words with an application to the automata-based approach for real addition.	Formal Methods in System Design	2008	DBLP DOI BibTeX RDF	Mixed linear arithmetic over the integers and reals, Verification of infinite-state systems, Decision procedure, Automata theory
1	Li Li, Xiaoyu Song, Ming Gu, Jianmin Wang 0001	A Maximum Weight Heuristic Method for Abstract State Computation.	COMPSAC	2008	DBLP DOI BibTeX RDF	model checking, program verification, weight, predicate abstraction
1	Clare Dixon, Michael Fisher, Boris Konev, Alexei Lisitsa	Practical First-Order Temporal Reasoning.	TIME	2008	DBLP DOI BibTeX RDF
1	Paolo Baldan, Andrea Corradini, Barbara König	Unfolding Graph Transformation Systems: Theory and Applications to Verification.	Concurrency, Graphs and Models	2008	DBLP DOI BibTeX RDF
1	Benoît Boyer, Thomas Genet, Thomas P. Jensen	Certifying a Tree Automata Completion Checker.	IJCAR	2008	DBLP DOI BibTeX RDF
1	Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, Daniele Zucchelli	Towards SMT Model Checking of Array-Based Systems.	IJCAR	2008	DBLP DOI BibTeX RDF
1	Axel Legay	T(O)RMC: A Tool for (omega)-Regular Model Checking.	CAV	2008	DBLP DOI BibTeX RDF
1	Therese Berg, Bengt Jonsson, Harald Raffelt	Regular Inference for State Machines Using Domains with Equality Tests.	FASE	2008	DBLP DOI BibTeX RDF
1	George Jiroveanu, René K. Boel, Behzad Bordbar	On-Line Monitoring of Large Petri Net Models Under Partial Observation.	Discrete Event Dynamic Systems	2008	DBLP DOI BibTeX RDF	Monitoring, Diagnosis, DES
1	Aaron R. Bradley, Zohar Manna	Property-directed incremental invariant generation.	Formal Asp. Comput.	2008	DBLP DOI BibTeX RDF	Polynomial invariants, Clausal invariants, Model checking, Static analysis, Affine invariants, Invariant generation
1	Tobias Schüle	Verification of infinite state systems using Presburger arithmetic.		2007	RDF
1	Supratik Mukhopadhyay	A uniform constraint-based framework for the verification of infinite state systems.		2007	RDF
1	Yoshinobu Kawabe, Ken Mano, Hideki Sakurada, Yasuyuki Tsukada	Theorem-proving anonymity of infinite-state systems.	Inf. Process. Lett.	2007	DBLP DOI BibTeX RDF
1	Clare Dixon, Michael Fisher, Boris Konev, Alexei Lisitsa	Efficient First-Order Temporal Logic for Infinite-State Systems	CoRR	2007	DBLP BibTeX RDF
1	Silvio Ghilardi, Silvio Ranise, Enrica Nicolini, Daniele Zucchelli	From Non-Disjoint Combination to Satisfiability and Model-Checking of Infinite State Systems.	Deduction and Decision Procedures	2007	DBLP BibTeX RDF
1	Santiago Escobar, José Meseguer	Symbolic Model Checking of Infinite-State Systems Using Narrowing.	RTA	2007	DBLP DOI BibTeX RDF
1	Martin Fränzle, Christian Herde	HySAT: An efficient proof engine for bounded model checking of hybrid systems.	Formal Methods in System Design	2007	DBLP DOI BibTeX RDF	Verification, Hybrid systems, Satisfiability, Decision procedures, Bounded model checking, Infinite-state systems
1	Shuvendu K. Lahiri, Randal E. Bryant	Predicate abstraction with indexed predicates.	ACM Trans. Comput. Log.	2007	DBLP DOI BibTeX RDF	infinite-state verification, invariant synthesis, Formal verification, abstract interpretation, cache-coherence protocols, predicate abstraction
1	Ranko Lazic, Thomas Christopher Newcomb, Joël Ouaknine, A. W. Roscoe, James Worrell	Nets with Tokens Which Carry Data.	ICATPN	2007	DBLP DOI BibTeX RDF
1	Jörg Bauer 0001, Tobe Toben, Bernd Westphal	Mind the Shapes: Abstraction Refinement Via Topology Invariants.	ATVA	2007	DBLP DOI BibTeX RDF
1	Bengt Jonsson, Mayank Saksena	Systematic Acceleration in Regular Model Checking.	CAV	2007	DBLP DOI BibTeX RDF
1	Benjamin Aminof, Aniello Murano, Moshe Y. Vardi	Pushdown Module Checking with Imperfect Information.	CONCUR	2007	DBLP DOI BibTeX RDF
1	Rohit Chadha, Mahesh Viswanathan	Decidability Results for Well-Structured Transition Systems with Auxiliary Storage.	CONCUR	2007	DBLP DOI BibTeX RDF
1	Ahmed Bouajjani, Peter Habermehl, Yan Jurski, Mihaela Sighireanu	Rewriting Systems with Data.	FCT	2007	DBLP DOI BibTeX RDF
1	Jérôme Leroux, Grégoire Sutre	Acceleration in Convex Data-Flow Analysis.	FSTTCS	2007	DBLP DOI BibTeX RDF
1	Alessandro Ferrante, Aniello Murano, Mimmo Parente	Enriched µ-Calculus Pushdown Module Checking.	LPAR	2007	DBLP DOI BibTeX RDF
1	Jan Olaf Blech, Ina Schaefer, Arnd Poetzsch-Heffter	Translation Validation of System Abstractions.	RV	2007	DBLP DOI BibTeX RDF
1	Frédéric Herbreteau, Grégoire Sutre, The Quang Tran	Unfolding Concurrent Well-Structured Transition Systems.	TACAS	2007	DBLP DOI BibTeX RDF
1	Felix Klaedtke, Stefan Ratschan, Zhikun She	Language-Based Abstraction Refinement for Hybrid System Verification.	VMCAI	2007	DBLP DOI BibTeX RDF
1	Antonín Kucera, Ph. Schnoebelen	A general approach to comparing infinite-state systems with their finite-state specifications.	Theor. Comput. Sci.	2006	DBLP DOI BibTeX RDF
1	Hsu-Chun Yen, Lien-Po Yu	Decidability Analysis of Self-Stabilization for Infinite-State Systems.	Fundam. Inform.	2006	DBLP BibTeX RDF
1	Antonín Kucera, Petr Jancar	Equivalence-checking on infinite-state systems: Techniques and results.	TPLP	2006	DBLP DOI BibTeX RDF
1	Randal E. Bryant	Formal Verification of Infinite State Systems Using Boolean Methods.	RTA	2006	DBLP DOI BibTeX RDF
1	Edmund M. Clarke, Marius Minea, Ferucio Laurentiu Tiplea (eds.)	Verification of Infinite-State Systems with Applications to Security, Proceedings of the NATO Advanced Research Workshop "Verification of Infinite State Systems with Applications to Security VISSAS 2005", Timisoara, Romania, March 17-22, 2005	VISSAS	2006	DBLP BibTeX RDF
1	Basil Becker, Dirk Beyer, Holger Giese, Florian Klein, Daniela Schilling	Symbolic invariant verification for systems with dynamic structural adaptation.	ICSE	2006	DBLP DOI BibTeX RDF	gormal verification, hraph transformation systems, structural invariants, transition invariants, embedded systems, mechatronics, symbolic algorithms