Gourinath Banda & John P. Gallagher (2010):
Constraint-based Abstract Semantics for Temporal Logic: A Direct Approach to Design and Implementation.
In: Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning,
LPAR'10,
doi:10.1007/978-3-642-17511-4_3.
Tewodros A. Beyene, Corneliu Popeea & Andrey Rybalchenko (2013):
Solving Existentially Quantified Horn Clauses.
In: Proceedings of the 25th International Conference on Computer Aided Verification,
CAV'13,
doi:10.1007/978-3-642-39799-8_61.
Aaron R. Bradley, Zohar Manna & Henny B. Sipma (2005):
Polyranking for Polynomial Loops.
Automata, Languages and Programming,
pp. 1349–1361.
J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill & L.J. Hwang (1990):
Symbolic model checking: 10^20 states and beyond,
doi:10.1016/0890-5401(92)90017-A.
Sagar Chaki, Edmund M. Clarke, Orna Grumberg, Joël Ouaknine, Natasha Sharygina, Tayssir Touili & Helmut Veith (2005):
State/Event Software Verification for Branching-Time Specifications..
In: IFM 3771.
Springer,
pp. 53–69,
doi:10.1007/11589976_5.
E. M. Clarke, E. A. Emerson & A. P. Sistla (1983):
Automatic Verification of Finite State Concurrent System Using Temporal Logic Specifications: A Practical Approach.
In: Proceedings of the 10th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages,
POPL '83,
doi:10.1145/567067.567080.
Edmund Clarke, Yuan Lu, Broadcom Com, Helmut Veith & Somesh Jha (2002):
Tree-Like Counterexamples in Model Checking.
In: In Proceedings of the 17 th Annual IEEE Symposium on Logic in Computer Science (LICS’02).
IEEE Computer Society,
doi:10.1109/LICS.2002.1029814.
Edmund M. Clarke (1991):
Temporal Logic Model Checking: Two Techniques for Avoiding the State Explosion Problem.
CAV '90.
Byron Cook & Eric Koskinen (2013):
Reasoning about Nondeterminism in Programs.
In: PLDI,
doi:10.1145/2491956.2491969.
Byron Cook, Eric Koskinen & Moshe Vardi (2012):
Temporal Property Verification As a Program Analysis Task.
Form. Methods Syst. Des.,
doi:10.1007/s10703-012-0153-5.
Byron Cook, Andreas Podelski & Andrey Rybalchenko (2006):
Termination proofs for systems code.
In: PLDI,
doi:10.1145/1133981.1134029.
Stéphane Demri, Alain Finkel, Valentin Goranko Govert & Van Drimmelen (2010):
Model checking CTL* over flat Presburger counter systems.
JANCL,
doi:10.3166/jancl.20.313-344.
E. Allen Emerson (1990):
Handbook of Theoretical Computer Science (Vol. B), chapter Temporal and Modal Logic.
E. Allen Emerson & Kedar S. Namjoshi (1996):
Automatic Verification of Parameterized Synchronous Systems (Extended Abstract).
In: Proceedings of the 8th International Conference on Computer Aided Verification,
CAV '96,
doi:10.1007/3-540-61474-5_60.
Sergey Grebenshchikov, Ashutosh Gupta, Nuno P. Lopes, Corneliu Popeea & Andrey Rybalchenko (2012):
HSF(C): A Software Verifier Based on Horn Clauses.
In: TACAS,
doi:10.1007/978-3-642-28756-5_46.
Ashutosh Gupta, Thomas A. Henzinger, Rupak Majumdar, Andrey Rybalchenko & Ru-Gang Xu (2008):
Proving non-termination.
In: POPL,
doi:10.1145/1328438.1328459.
Arie Gurfinkel, Ou Wei & Marsha Chechik (2006):
Yasm: A Software Model-Checker for Verification and Refutation..
In: Thomas Ball & Robert B. Jones: CAV,
Lecture Notes in Computer Science.
Springer,
pp. 170–174,
doi:10.1007/11817963_18.
Zyad Hassan, Aaron R. Bradley & Fabio Somenzi (2012):
Incremental, Inductive CTL Model Checking.
In: Proceedings of the 24th International Conference on Computer Aided Verification,
doi:10.1007/978-3-642-31424-7_38.
Krystof Hoder, Nikolaj Bjørner & Leonardo de Moura (2011):
μZ- An Efficient Engine for Fixed Points with Constraints.
In: CAV,
doi:10.1007/978-3-642-22110-1_36.
Yonit Kesten & Amir Pnueli (2005):
A compositional approach to CTL* verification.
Theor. Comput. Sci. 331(2-3),
pp. 397–428,
doi:10.1016/j.tcs.2004.09.023.
Orna Kupferman, Moshe Y. Vardi & Pierre Wolper (2000):
An Automata-theoretic Approach to Branching-time Model Checking.
J. ACM,
doi:10.1145/333979.333987.
Zohar Manna & Amir Pnueli (1992):
The Temporal Logic of Reactive and Concurrent Systems.
Springer-Verlag New York, Inc.,
New York, NY, USA,
doi:10.1007/978-1-4612-0931-7.
Wojciech Penczek, Bozena Wozna & Andrzej Zbrzezny (2002):
Bounded Model Checking for the Universal Fragment of CTL.
Fundam. Inf..
Amir Pnueli (1977):
The Temporal Logic of Programs.
In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science,
doi:10.1109/SFCS.1977.32.
Fu Song & Tayssir Touili (2011):
Efficient CTL model-checking for pushdown systems.
In: In CONCUR,
doi:10.1007/978-3-642-23217-6_29.
Fu Song & Tayssir Touili (2013):
PoMMaDe: Pushdown Model-checking for Malware Detection.
In: Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering.
ACM,
doi:10.1007/978-3-642-28756-5_9.
Igor Walukiewicz (2000):
Model Checking CTL Properties of Pushdown Systems..
In: FSTTCS,
Lecture Notes in Computer Science,
doi:10.1007/3-540-44450-5_10.
Igor Walukiewicz (2001):
Pushdown processes: Games and model-checking.
Information and computation,
doi:10.1007/3-540-61474-5_58.
eptcs@eptcs.org