Abstract is missing.
- Interpolation and SAT-Based Model CheckingKenneth L. McMillan. 1-13 [doi]
- Bounded Model Checking and Induction: From Refutation to Verification (Extended Abstract, Category A)Leonardo Mendonça de Moura, Harald Rueß, Maria Sorea. 14-26 [doi]
- Reasoning with Temporal Logic on Truncated PathsCindy Eisner, Dana Fisman, John Havlicek, Yoad Lustig, Anthony McIsaac, David Van Campenhout. 27-39 [doi]
- Structural Symbolic CTL Model Checking of Asynchronous SystemsGianfranco Ciardo, Radu Siminiceanu. 40-53 [doi]
- A Work-Efficient Distributed Algorithm for Reachability AnalysisOrna Grumberg, Tamir Heyman, Assaf Schuster. 54-66 [doi]
- Modular Strategies for Infinite Games on Recursive GraphsRajeev Alur, Salvatore La Torre, P. Madhusudan. 67-79 [doi]
- Fast Mu-Calculus Model Checking when Tree-Width Is BoundedJan Obdrzálek. 80-92 [doi]
- Dense Counter Machines and Verification ProblemsGaoyan Xie, Zhe Dang, Oscar H. Ibarra, Pierluigi San Pietro. 93-105 [doi]
- TRIM: A Tool for Triggered Message Sequence ChartsBikram Sengupta, Rance Cleaveland. 106-109 [doi]
- Model Checking Multi-Agent Programs with CASPRafael H. Bordini, Michael Fisher, Carmen Pardavila, Willem Visser, Michael Wooldridge. 110-113 [doi]
- Monitoring Temporal Rules Combined with Time SeriesDoron Drusinsky. 114-117 [doi]
- FAST: Fast Acceleration of Symbolikc Transition SystemsSébastien Bardin, Alain Finkel, Jérôme Leroux, Laure Petrucci. 118-121 [doi]
- Rabbit: A Tool for BDD-Based Verification of Real-Time SystemsDirk Beyer, Claus Lewerentz, Andreas Noack. 122-125 [doi]
- Making Predicate Abstraction Efficient: How to Eliminate Redundant PredicatesEdmund M. Clarke, Orna Grumberg, Muralidhar Talupur, Dong Wang. 126-140 [doi]
- A Symbolic Approach to Predicate AbstractionShuvendu K. Lahiri, Randal E. Bryant, Byron Cook. 141-153 [doi]
- Unbounded, Fully Symbolic Model Checking of Timed Automata using Boolean MethodsSanjit A. Seshia, Randal E. Bryant. 154-166 [doi]
- Digitizing Interval Duration LogicGaurav Chakravorty, Paritosh K. Pandya. 167-179 [doi]
- Timed Control with Partial ObservabilityPatricia Bouyer, Deepak D Souza, P. Madhusudan, Antoine Petit. 180-192 [doi]
- Hybrid Acceleration Using Real Vector Automata (Extended Abstract)Bernard Boigelot, Frédéric Herbreteau, Sébastien Jodogne. 193-205 [doi]
- Abstraction and BDDs Complement SAT-Based BMC in DiVerAarti Gupta, Malay K. Ganai, Chao Wang, Zijiang Yang, Pranav Ashar. 206-209 [doi]
- TLQSolver: A Temporal Logic Query CheckerMarsha Chechik, Arie Gurfinkel. 210-214 [doi]
- Evidence Explorer: A Tool for Exploring Model-Checking ProofsYifei Dong, C. R. Ramakrishnan, Scott A. Smolka. 215-218 [doi]
- HERMES: An Automatic Tool for Verification of Secrecy in Security ProtocolsLiana Bozga, Yassine Lakhnech, Michaël Périn. 219-222 [doi]
- Iterating Transducers in the Large (Extended Abstract)Bernard Boigelot, Axel Legay, Pierre Wolper. 223-235 [doi]
- Algorithmic Improvements in Regular Model CheckingParosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson, Julien d Orso. 236-248 [doi]
- Efficient Image Computation in Infinite State Model CheckingConstantinos Bartzis, Tevfik Bultan. 249-261 [doi]
- Thread-Modular Abstraction RefinementThomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Shaz Qadeer. 262-274 [doi]
- A Game-Based Framework for CTL Counterexamples and 3-Valued Abstraction-RefinementSharon Shoham, Orna Grumberg. 275-287 [doi]
- Abstraction for Branching Time PropertiesKedar S. Namjoshi. 288-300 [doi]
- Certifying Optimality of State Estimation ProgramsGrigore Rosu, Ram Prasad Venkatesan, Jon Whittle, Laurentiu Leustean. 301-314 [doi]
- Domain-Specific Optimization in Automata LearningHardi Hungar, Oliver Niese, Bernhard Steffen. 315-327 [doi]
- Model Checking Conformance with Scenario-Based SpecificationsMarcelo Glusman, Shmuel Katz. 328-340 [doi]
- Deductive Verification of Advanced Out-of-Order MicroprocessorsShuvendu K. Lahiri, Randal E. Bryant. 341-353 [doi]
- Theorem Proving Using Lazy Proof ExplicationCormac Flanagan, Rajeev Joshi, Xinming Ou, James B. Saxe. 355-367 [doi]
- Enhanced Vacuity Detection in Linear Temporal LogicRoy Armoni, Limor Fix, Alon Flaisher, Orna Grumberg, Nir Piterman, Andreas Tiemeyer, Moshe Y. Vardi. 368-380 [doi]
- Bridging the Gap between Fair Simulation and Trace InclusionYonit Kesten, Nir Piterman, Amir Pnueli. 381-393 [doi]
- An Improved On-The-Fly Tableau Construction for a Real-Time Temporal LogicMarc Geilen. 394-406 [doi]
- Strengthening Invariants by Symbolic Consistency TestingHusam Abu-Haimed, Sergey Berezin, David L. Dill. 407-419 [doi]
- Linear Invariant Generation Using Non-linear Constraint SolvingMichael Colón, Sriram Sankaranarayanan, Henny Sipma. 420-432 [doi]
- To Store or Not to StoreGerd Behrmann, Kim Guldstrand Larsen, Radek Pelánek. 433-445 [doi]
- Calculating-Confluence CompositionallyGordon J. Pace, Frédéric Lang, Radu Mateescu. 446-459 [doi]