49 papers:
LATA-2015-LuckMS #complexity #theorem- Parameterized Complexity of CTL — A Generalization of Courcelle’s Theorem (ML, AM, IS), pp. 549–560.
CADE-2015-Ji #deduction #model checking- CTL Model Checking in Deduction Modulo (KJ), pp. 295–310.
CAV-2015-CookKP #automation #infinity #on the #verification- On Automation of CTL* Verification for Infinite-State Systems (BC, HK, NP), pp. 13–29.
- CAV-2015-FinkbeinerRS #algorithm #model checking
- Algorithms for Model Checking HyperLTL and HyperCTL ^* (BF, MNR, CS), pp. 30–48.
FSE-2014-VakiliD #infinity #modelling #smt #using #verification- Verifying CTL-live properties of infinite state models using an SMT solver (AV, NAD), pp. 213–223.
SLE-2014-BillGKS #model checking #ocl #specification- Model Checking of CTL-Extended OCL Specifications (RB, SG, PK, MS), pp. 221–240.
IJCAR-2014-Gore #fixpoint #logic #ltl- And-Or Tableaux for Fixpoint Logics with Converse: LTL, CTL, PDL and CPDL (RG), pp. 26–45.
ASE-2012-SongT #model checking #named #source code- PuMoC: a CTL model-checker for sequential programs (FS, TT), pp. 346–349.
WRLA-2012-LepriAO #maude #model checking #realtime- Timed CTL Model Checking in Real-Time Maude (DL, EÁ, PCÖ), pp. 182–200.
- CAV-2012-HassanBS #incremental #induction #model checking
- Incremental, Inductive CTL Model Checking (ZH, ARB, FS), pp. 532–547.
ICEIS-v3-2011-WangWWL #modelling #using #workflow- Formally Modeling and Analyzing Data-centric Workflow using WFCP-net and ASK-CTL (ZW, JW, LW, GL), pp. 139–144.
FoSSaCS-2010-LaroussinieMP- Counting CTL (FL, AM, EP), pp. 206–220.
- CAV-2010-FerranteMNPS #model checking
- A NuSMV Extension for Graded-CTL Model Checking (AF, MM, MN, MP, FS), pp. 670–673.
- IJCAR-2010-FriedmannLL #automaton
- A Decision Procedure for CTL* Based on Tableaux and Automata (OF, ML, ML), pp. 331–345.
FM-2009-Reynolds- A Tableau for CTL (MR), pp. 403–418.
- CADE-2009-ZhangHD #calculus
- A Refined Resolution Calculus for CTL (LZ, UH, CD), pp. 245–260.
- FoSSaCS-2008-Bozzelli #complexity #linear
- The Complexity of CTL* + Linear Past (LB), pp. 186–200.
SEKE-2008-DingZ #case study #explosion #problem- A Study of the Model Explosion Problem in CTL Model Update (YD, YZ), pp. 752–757.
LICS-2008-BrazdilFKK #probability #problem #satisfiability- The Satisfiability Problem for Probabilistic CTL (TB, VF, JK, AK), pp. 391–402.
VMCAI-2008-JonesH- CTL as an Intermediate Language (NDJ, RRH), p. 4.
EDOC-2007-HalleVCG #model checking #workflow- Model Checking Data-Aware Workflow Properties with CTL-FO+ (SH, RV, OC, BG), pp. 267–278.
COCV-2007-FangS #bidirectional #compilation #generative #java #using- Generating Java Compiler Optimizers Using Bidirectional CTL (LF, MS), pp. 49–63.
AMOST-2007-WijesekeraASF #model checking #specification #testing- Relating counterexamples to test cases in CTL model checking specifications (DW, PA, LS, GF), pp. 75–84.
MBT-2006-SilvaM #generative #towards- Towards Test Purpose Generation from CTL Properties for Reactive Systems (DAdS, PDLM), pp. 29–40.
TACAS-2005-Marrero #using- Using BDDs to Decide CTL (WM), pp. 222–236.
QAPL-2004-Lluch-LafuenteM05 #calculus #constraints- Quantitative ?-calculus and CTL Based on Constraint Semirings (ALL, UM), pp. 37–59.
- TACAS-2004-ShohamG #abstraction
- Monotonic Abstraction-Refinement for CTL (SS, OG), pp. 546–560.
SEFM-2004-SistlaWZ #using- Checking Extended CTL properties Using Guarded Quotient Structures (APS, XW, MZ), pp. 87–94.
DAC-2003-JayakumarPS #estimation- Dos and don’ts of CTL state coverage estimation (NJ, MP, FS), pp. 292–295.
ICALP-2003-JohannsenL #exponential- CTL+ Is Complete for Double Exponential Time (JJ, ML), pp. 767–775.
- CAV-2003-CiardoS #model checking
- Structural Symbolic CTL Model Checking of Asynchronous Systems (GC, RS), pp. 40–53.
- CAV-2003-ShohamG #abstraction #framework #game studies
- A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-Refinement (SS, OG), pp. 275–287.
CSL-2003-SamerV #query #revisited- Validity of CTL Queries Revisited (MS, HV), pp. 470–483.
- CAV-2002-PurandareS
- Vacuum Cleaning CTL Formulae (MP, FS), pp. 485–499.
- FoSSaCS-2001-LaroussinieMS #model checking
- Model Checking CTL+ and FCTL is Hard (FL, NM, PS), pp. 318–331.
- TACAS-2001-Pandya #model checking
- Model Checking CTL*[DC] (PKP), pp. 559–573.
- DAC-2000-BloemRS #model checking
- Symbolic guided search for CTL model checking (RB, KR, FS), pp. 29–34.
DATE-2000-JangMH #model checking- Iterative Abstraction-Based CTL Model Checking (JYJ, IHM, GDH), pp. 502–507.
- CAV-1999-Lind-NielsenA #model checking
- Stepwise CTL Model Checking of State/Event Systems (JLN, HRA), pp. 316–327.
- LICS-1999-MollerR #on the #power of
- On the Expressive Power of CTL (FM, AMR), pp. 360–368.
- DAC-1998-PardoH #incremental #model checking #using
- Incremental CTL Model Checking Using BDD Subsetting (AP, GDH), pp. 457–462.
- LICS-1995-BhatCG #model checking #on the fly #performance
- Efficient On-the-Fly Model Checking for CTL* (GB, RC, OG), pp. 388–397.
- CAV-1994-AzizSS #composition #equivalence #model checking
- Formula-Dependent Equivalence for Compositional CTL Model Checking (AA, TRS, VS), pp. 324–337.
- DAC-1993-HojatiSBK #approach #model checking
- A Unified Approach to Language Containment and Fair CTL Model Checking (RH, TRS, RKB, RPK), pp. 475–481.
- CAV-1993-DamsGG #generative #modelling
- Generation of Reduced Models for Checking Fragments of CTL (DD, OG, RG), pp. 479–490.
- CAV-1993-HojatiBK #debugging #design #using
- BDD-Based Debugging Of Design Using Language Containment and Fair CTL (RH, RKB, RPK), pp. 41–58.
- CAV-1992-ShipleCSB #automation #composition #model checking #reduction
- Automatic Reduction in CTL Compositional Model Checking (TRS, MC, ALSV, RKB), pp. 234–247.
- ICALP-1987-HaferT #logic #monad #quantifier
- Computation Tree Logic CTL* and Path Quantifiers in the Monadic Theory of the Binary Tree (TH, WT), pp. 269–279.
- ICALP-1987-Josko #liveness #model checking
- Modelchecking of CTL Formulae under Liveness Assumptions (BJ), pp. 280–289.
