Abstract is missing.
- SMT-Based Model CheckingCesare Tinelli. 1 [doi]
- Verified Software ToolchainAndrew W. Appel. 2 [doi]
- Formal Verification by Abstract InterpretationPatrick Cousot. 3-7 [doi]
- Quantitative Timed Analysis of Interactive Markov ChainsDennis Guck, Tingting Han, Joost-Pieter Katoen, Martin R. Neuhäußer. 8-23 [doi]
- Lessons Learnt from the Adoption of Formal Model-Based DevelopmentAlessio Ferrari, Alessandro Fantechi, Stefania Gnesi. 24-38 [doi]
- Symbolic Execution of Communicating and Hierarchically Composed UML-RT State MachinesKarolina Zurowska, Jürgen Dingel. 39-53 [doi]
- Inferring Definite Counterexamples through Under-ApproximationJörg Brauer, Axel Simon. 54-69 [doi]
- Modifying Test Suite Composition to Enable Effective Predicate-Level Statistical DebuggingRoss Gore, Paul F. Reynolds Jr.. 70-84 [doi]
- Rigorous Polynomial Approximation Using Taylor Models in CoqNicolas Brisebarre, Mioara Joldes, Érik Martin-Dorel, Micaela Mayero, Jean-Michel Muller, Ioana Pasca, Laurence Rideau, Laurent Théry. 85-99 [doi]
- Enhancing the Inverse Method with State MergingÉtienne André, Laurent Fribourg, Romain Soulat. 100-105 [doi]
- Class-Modular, Class-Escape and Points-to Analysis for Object-Oriented LanguagesAlexander Herz, Kalmer Apinis. 106-119 [doi]
- Testing Static Analyzers with Randomly Generated ProgramsPascal Cuoq, Benjamin Monate, Anne Pacalet, Virgile Prevosto, John Regehr, Boris Yakobowski, Xuejun Yang. 120-125 [doi]
- Compositional Verification of Architectural ModelsDarren D. Cofer, Andrew Gacek, Steven P. Miller, Michael W. Whalen, Brian LaValley, Lui Sha. 126-140 [doi]
- A Safety Case Pattern for Model-Based Development ApproachAnaheed Ayoub, BaekGyu Kim, Insup Lee, Oleg Sokolsky. 141-146 [doi]
- PVS Linear Algebra Libraries for Verification of Control Software Algorithms in C/ACSLHeber Herencia-Zapana, Romain Jobredeaux, Sam Owre, Pierre-Loïc Garoche, Eric Feron, Gilberto Perez, Pablo Ascariz. 147-161 [doi]
- Temporal Action Language (TAL): A Controlled Language for Consistency Checking of Natural Language Temporal Requirements - (Preliminary Results)Wenbin Li, Jane Huffman Hayes, Miroslaw Truszczynski. 162-167 [doi]
- Some Steps into Verification of Exact Real ArithmeticNorbert Th. Müller, Christian Uhrhan. 168-173 [doi]
- Runtime Verification Meets Android SecurityAndreas Bauer 0002, Jan-Christoph Küster, Gil Vegliach. 174-180 [doi]
- Specification in PDL with RecursionXinxin Liu, Bingtian Xue. 181-194 [doi]
- Automatically Proving Thousands of Verification Conditions Using an SMT Solver: An Empirical StudyAditi Tagore, Diego Zaccai, Bruce W. Weide. 195-209 [doi]
- Sound Formal Verification of Linux's USB BP Keyboard DriverWillem Penninckx, Jan Tobias Mühlberg, Jan Smans, Bart Jacobs, Frank Piessens. 210-215 [doi]
- Learning Markov Models for Stationary System BehaviorsYingke Chen, Hua Mao, Manfred Jaeger, Thomas Dyhre Nielsen, Kim Guldstrand Larsen, Brian Nielsen. 216-230 [doi]
- The Use of Rippling to Automate Event-B Invariant Preservation ProofsYuhui Lin, Alan Bundy, Gudmund Grov. 231-236 [doi]
- Thread-Modular Model Checking with Iterative RefinementWenrui Meng, Fei He, Bow-Yaw Wang, Qiang Liu. 237-251 [doi]
- Towards LTL Model Checking of Unmodified Thread-Based C & C++ ProgramsJiri Barnat, Lubos Brim, Petr Rockai. 252-266 [doi]
- Integrating Statechart Components in PolyglotDaniel Balasubramanian, Corina S. Pasareanu, Jason Biatek, Thomas Pressburger, Gabor Karsai, Michael R. Lowry, Michael W. Whalen. 267-272 [doi]
- Using PVS to Investigate Incidents through the Lens of Distributed CognitionPaolo Masci, Huayi Huang, Paul Curzon, Michael D. Harrison. 273-278 [doi]
- Automated Analysis of Parametric Timing-Based Mutual Exclusion AlgorithmsRoberto Bruttomesso, Alessandro Carioni, Silvio Ghilardi, Silvio Ranise. 279-294 [doi]
- Efficient Symbolic Execution of Value-Based Data Structures for Critical SystemsJason Belt, Robby, Patrice Chalin, John Hatcliff, Xianghua Deng. 295-309 [doi]
- Generating Verifiable Java Code from Verified PVS SpecificationsLeonard Lensink, Sjaak Smetsers, Marko C. J. D. van Eekelen. 310-325 [doi]
- Belief Bisimulation for Hidden Markov Models - Logical Characterisation and Decision AlgorithmDavid N. Jansen, Flemming Nielson, Lijun Zhang 0001. 326-340 [doi]
- Abstract Model RepairGeorge Chatzieleftheriou, Borzoo Bonakdarpour, Scott A. Smolka, Panagiotis Katsaros. 341-355 [doi]
- CLSE: Closed-Loop Symbolic ExecutionRupak Majumdar, Indranil Saha, K. C. Shashidhar, Zilong Wang. 356-370 [doi]
- On the Development and Formalization of an Extensible Code Generator for Real Life Security ProtocolsMichael Backes, Alex Busenius, Catalin Hritcu. 371-387 [doi]
- Incremental Verification with Mode Variable Invariants in State MachinesTemesghen Kahsai, Pierre-Loïc Garoche, Cesare Tinelli, Mike Whalen. 388-402 [doi]
- A Semantic Analysis of Wireless Network Security ProtocolsDamiano Macedonio, Massimo Merro. 403-417 [doi]
- Runtime Verification with Predictive SemanticsXian Zhang, Martin Leucker, Wei Dong. 418-432 [doi]
- A Case Study in Verification of Embedded Network SoftwareKalyan C. Regula, Hampton Smith, Heather Keown, Jason O. Hallstrom, Nigamanth Sridhar, Murali Sitaraman. 433-448 [doi]
- Checking and Distributing Statistical Model CheckingPeter E. Bulychev, Alexandre David, Kim Guldstrand Larsen, Axel Legay, Marius Mikucionis, Danny Bøgsted Poulsen. 449-463 [doi]