title: Parameterized Synthesis with Safety Properties

authors:
Oliver Markgraf
Chih-Duo Hong
Anthony W. Lin
Muhammad Najib
Daniel Neider

abstract: Parameterized synthesis offers a solution to the problem of constructing correct and verified controllers for parameterized systems. Such systems occur naturally in practice (e.g., in the form of distributed protocols where the amount of processes is often unknown at design time and the protocol must work regardless of the number of processes). In this paper, we present a novel learning based approach to the synthesis of reactive controllers for parameterized systems from safety specifications. We use the framework of regular model checking to model the synthesis problem as an infinite-duration two-player game and show how one can utilize Angluin's well-known L* algorithm to learn correct-by-design controllers. This approach results in a synthesis procedure that is conceptually simpler than existing synthesis methods with a completeness guarantee, whenever a winning strategy can be expressed by a regular set. We have implemented our algorithm in a tool called L*-PSynth and have demonstrated its performance on a range of benchmarks, including robotic motion planning and distributed protocols. Despite the simplicity of L*-PSynth it competes well against (and in many cases even outperforms) the state-of-the-art tools for synthesizing parameterized systems.


venue: aplas

title: Stack-Driven Program Generation of WebAssembly

authors:
Árpád Perényi
Jan Midtgaard


title: P3: A Profiler Suite for Parallel Applications on the Java Virtual Machine

authors:
Andrea Rosà
Walter Binder


title: Certified Semantics for Relational Programming

authors:
Dmitry Rozplokhas
Andrey Vyatkin
Dmitry Boulytchev

abstract: We present a formal study of semantics for relational programming language miniKanren. First, we formulate denotational semantics which corresponds to the minimal Herbrand model for definite logic programs. Second, we present operational semantics which models the distinctive feature of miniKanren implementation -- interleaving, -- and prove its soundness and completeness w.r.t. the denotational semantics. Our development is supported by a Coq specification, from which a reference interpreter can be extracted. We also derive from our main result a certified semantics (and a reference interpreter) for SLD resolution with cut and prove its soundness.


title: REFINITY to Model and Prove Program Transformation Rules


title: A Counterexample-Guided Debugger for Non-recursive Datalog

authors:
Van-Dang Tran
Hiroyuki Kato
Zhenjiang Hu


title: Algebraic and Coalgebraic Perspectives on Interaction Laws

authors:
Tarmo Uustalu
Niels F. W. Voorneveld


title: Fully Abstract and Robust Compilation: And How to Reconcile the Two, Abstractly

authors:
Carmine Abate
Matteo Busi
Stelios Tsampas


title: Solving Not-Substring Constraint withFlat Abstraction

authors:
Parosh Aziz Abdulla
Mohamed Faouzi Atig
Yu-Fang Chen
Bui Phi Diep
Lukás Holík
Denghang Hu
Wei-Lun Tsai
Zhilin Wu
Di-De Yen


title: Adaptable Traces for Program Explanations

authors:
Divya Bajaj
Martin Erwig
Danila Fedorin
Kai Gay


title: Latent Effects for Reusable Language Components

authors:
Birthe van den Berg
Tom Schrijvers
Casper Bach Poulsen
Nicolas Wu


title: Hybrid Quantum-Classical Circuit Simplification with the ZX-Calculus

authors:
Agustín Borgna
Simon Perdrix
Benoît Valiron

abstract: We present a complete optimization procedure for hybrid quantum-classical circuits with classical parity logic. While common optimization techniques for quantum algorithms focus on rewriting solely the pure quantum segments, there is interest in applying a global optimization process for applications such as quantum error correction and quantum assertions. This work, based on the pure-quantum circuit optimization procedure by Duncan et al., uses an extension of the formal graphical ZX-calculus called ZX-ground as an intermediary representation of the hybrid circuits to allow for granular optimizations below the quantum-gate level. We define a translation from hybrid circuits into diagrams that admit the graph-theoretical focused-gFlow property, needed for the final extraction back into a circuit. We then derive a number of gFlow-preserving optimization rules for ZX-ground diagrams that reduce the size of the graph, and devise an strategy to find optimization opportunities by rewriting the diagram guided by a Gauss elimination process. Then, after extracting the circuit, we present a general procedure for detecting segments of circuit-like ZX-ground diagrams which can be implemented with classical gates in the extracted circuit. We have implemented our optimization procedure as an extension to the open-source python library PyZX.


title: PyCT: A Python Concolic Tester

authors:
Yu-Fang Chen
Wei-Lun Tsai
Wei-Cheng Wu
Di-De Yen
Fang Yu


title: Program Synthesis for Musicians: A Usability Testbed for Temporal Logic Specifications

authors:
Wonhyuk Choi
Michel Vazirani
Mark Santolucito


title: A Typed Programmatic Interface to Contracts on the Blockchain

authors:
Thi Thu Ha Doan
Peter Thiemann

abstract: Smart contract applications on the blockchain can only reach their full potential if they integrate seamlessly with traditional software systems via a programmatic interface. This interface should provide for originating and invoking contracts as well as observing the state of the blockchain. We propose a typed API for this purpose and establish some properties of the combined system. Specifically, we provide an execution model that enables us to prove type-safe interaction between programs and the blockchain. We establish further properties of the model that give rise to requirements on the API. A prototype of the interface is implemented in OCaml for the Tezos blockchain.


title: The Choice Construct in the Soufflé Language

authors:
Xiaowen Hu
Joshua Karp
David Zhao
Abdul Zreika
Xi Wu
Bernhard Scholz

abstract: Datalog has become a popular implementation language for solving large-scale, real-world problems, including bug finders, network analysis tools, and disassemblers. These applications express complex behaviour with hundreds of relations and rules that often require a non-deterministic choice for tuples in relations to express worklist algorithms. This work is an experience report that describes the implementation of a choice construct in the Datalog engine Souffle. With the choice construct, we can express worklist algorithms such as spanning trees in a few lines of code. We highlight the differences between rule-based choice as described in prior work, and relation-based choice introduced by this work. We show that a choice construct enables certain worklist algorithms to be computed up to 10kx faster than having no choice construct.


title: Server-Side Computation of Package Dependencies in Package-Management Systems

authors:
Nobuhiro Kasai
Isao Sasano


title: Function Pointer Eliminator for C Programs

authors:
Daisuke Kimura
Mahmudul Faisal Al Ameen
Makoto Tatsuta
Koji Nakazawa


title: Proving LTL Properties of Bitvector Programs and Decompiled Binaries

authors:
Yuandong Cyrus Liu
Chengbin Pang
Daniel Dietsch
Eric Koskinen
Ton-Chanh Le
Georgios Portokalidis
Jun Xu

abstract: There is increasing interest in applying verification tools to programs that have bitvector operations (eg., binaries). SMT solvers, which serve as a foundation for these tools, have thus increased support for bitvector reasoning through bit-blasting and linear arithmetic approximations. In this paper we show that similar linear arithmetic approximation of bitvector operations can be done at the source level through transformations. Specifically, we introduce new paths that over-approximate bitvector operations with linear conditions/constraints, increasing branching but allowing us to better exploit the well-developed integer reasoning and interpolation of verification tools. We show that, for reachability of bitvector programs, increased branching incurs negligible overhead yet, when combined with integer interpolation optimizations, enables more programs to be verified. We further show this exploitation of integer interpolation in the common case also enables competitive termination verification of bitvector programs and leads to the first effective technique for LTL verification of bitvector programs. Finally, we provide an in-depth case study of decompiled ("lifted") binary programs, which emulate X86 execution through frequent use of bitvector operations. We present a new tool DarkSea, the first tool capable of verifying reachability, termination, and LTL of lifted binaries.


title: A Compilation Method for Dynamic Typing in ML

authors:
Atsushi Ohori
Katsuhiro Ueno


title: Termination Analysis for the $$\pi $$-Calculus by Reduction to Sequential Program Termination

authors:
Tsubasa Shoshi
Takuma Ishikawa
Naoki Kobayashi
Ken Sakayori
Ryosuke Sato
Takeshi Tsukada

abstract: We propose an automated method for proving termination of $\pi$-calculus processes, based on a reduction to termination of sequential programs: we translate a $\pi$-calculus process to a sequential program, so that the termination of the latter implies that of the former. We can then use an off-the-shelf termination verification tool to check termination of the sequential program. Our approach has been partially inspired by Deng and Sangiorgi's termination analysis for the $\pi$-calculus, and checks that there is no infinite chain of communications on replicated input channels, by converting such a chain of communications to a chain of recursive function calls in the target sequential program. We have implemented an automated tool based on the proposed method and confirmed its effectiveness.


title: A Dictionary-Passing Translation of Featherweight Go

authors:
Martin Sulzmann
Stefan Wehr

abstract:
The Go programming language is an increasingly popular language but some of
its features lack a formal investigation.
This article explains Go's resolution mechanism for overloaded methods and
its support for structural subtyping by
means of translation from Featherweight Go to a simple target language.
The translation employs a form of dictionary passing known from type classes
in Haskell and preserves the
dynamic behavior of Featherweight Go programs.


title: Simplifying Alternating Automata for Emptiness Testing

authors:
Pavol Vargovcík
Lukás Holík


title: Scalable and Modular Robustness Analysis of Deep Neural Networks

authors:
Yuyi Zhong
Quang-Trung Ta
Tianzuo Luo
Fanlong Zhang
Siau-Cheng Khoo

abstract: As neural networks are trained to be deeper and larger, the scalability of neural network analyzers is urgently required. The main technical insight of our method is modularly analyzing neural networks by segmenting a network into blocks and conduct the analysis for each block. In particular, we propose the network block summarization technique to capture the behaviors within a network block using a block summary and leverage the summary to speed up the analysis process. We instantiate our method in the context of a CPU-version of the state-of-the-art analyzer DeepPoly and name our system as Bounded-Block Poly (BBPoly). We evaluate BBPoly extensively on various experiment settings. The experimental result indicates that our method yields comparable precision as DeepPoly but runs faster and requires less computational resources. For example, BBPoly can analyze really large neural networks like SkipNet or ResNet which contain up to one million neurons in less than around 1 hour per input image, while DeepPoly needs to spend even 40 hours to analyze one image.


title: Decoupling the Ascending and Descending Phases in Abstract Interpretation

authors:
Vincenzo Arceri
Isabella Mastroeni
Enea Zaffanella


title: Model-Based Fault Classification for Automotive Software

authors:
Mike Becker
Roland Meyer
Tobias Runge
Ina Schaefer
Sören van der Wall
Sebastian Wolff

abstract: Intensive testing using model-based approaches is the standard way of demonstrating the correctness of automotive software. Unfortunately, state-of-the-art techniques leave a crucial and labor intensive task to the test engineer: identifying bugs in failing tests. Our contribution is a model-based classification algorithm for failing tests that assists the engineer when identifying bugs. It consists of three steps. (i) Fault localization replays the test on the model to identify the moment when the two diverge. (ii) Fault explanation then computes the reason for the divergence. The reason is a subset of actions from the test that is sufficient for divergence. (iii) Fault classification groups together tests that fail for similar reasons. Our approach relies on machinery from formal methods: (i) symbolic execution, (ii) Hoare logic and a new relationship between the intermediary assertions constructed for a test, and (iii) a new relationship among Hoare proofs. A crucial aspect in automotive software is timing requirements, for which we develop appropriate Hoare logic theory. We also briefly report on our prototype implementation for the CAN bus Unified Diagnostic Services in an industrial project.


title: RHLE: Modular Deductive Verification of Relational ∀ ∃ Properties

authors:
Robert Dickerson
Qianchuan Ye
Michael K. Zhang
Benjamin Delaware

abstract: Relational program logics are used to prove that a desired relationship holds between the execution of multiple programs. Existing relational program logics have focused on verifying that all runs of a collection of programs do not fall outside a desired set of behaviors. Several important relational properties, including refinement and noninterference, do not fit into this category, as they require the existence of specific desirable executions. This paper presents RHLE, a logic for verifying a class of relational properties which we term $\forall\exists$ properties. $\forall\exists$ properties assert that for all executions of a collection of programs, there exist executions of another set of programs exhibiting some intended behavior. Importantly, RHLE can reason modularly about programs which make library calls, ensuring that $\forall\exists$ properties are preserved when the programs are linked with any valid implementation of the library. To achieve this, we develop a novel form of function specification that requires the existence of certain behaviors in valid implementations. We have built a tool based on RHLE which we use to verify a diverse set of relational properties drawn from the literature, including refinement and generalized noninterference.


title: An Algebraic Theory for Shared-State Concurrency

authors:
Yotam Dvir
Ohad Kammar
Ori Lahav

abstract: . We present a monadic denotational semantics for a higher-order programming language with shared-state concurrency, i.e


title: Novice Type Error Diagnosis with Natural Language Models

authors:
Chuqin Geng
Haolin Ye
Yixuan Li
Tianyu Han
Brigitte Pientka
Xujie Si


title: Characterizing Functions Mappable over GADTs

authors:
Patricia Johann
Pierre Cagne


title: Inferring Region Types via an Abstract Notion of Environment Transformation

authors:
Ulrich Schöpp
Chuangjie Xu


title: Automated Temporal Verification for Algebraic Effects

authors:
Yahui Song
Darius Foo
Wei-Ngan Chin


title: Applicative Intersection Types

authors:
Xu Xue
Bruno C. d. S. Oliveira
Ningning Xie


title: A Calculus with Recursive Types, Record Concatenation and Subtyping

authors:
Yaoda Zhou
Bruno C. d. S. Oliveira
Andong Fan


title: A Diamond Machine for Strong Evaluation

authors:
Beniamino Accattoli
Pablo Barenbaum


title: Oracle Computability and Turing Reducibility in the Calculus of Inductive Constructions

authors:
Yannick Forster
Dominik Kirst
Niklas Mück


title: m-CFA Exhibits Perfect Stack Precision


title: Typed Non-determinism in Functional and Concurrent Calculi

authors:
Bas van den Heuvel
Joseph W. N. Paulus
Daniele Nantes-Sobrinho
Jorge A. Pérez


title: Argument Reduction of Constrained Horn Clauses Using Equality Constraints

authors:
Ryo Ikeda
Ryosuke Sato
Naoki Kobayashi


abstract: Multiple types can represent the same concept. For example, lists and trees can both represent sets. Unfortunately, this easily leads to incomplete libraries: some set-operations may only be available on lists, others only on trees. Similarly, subtypes and quotients are commonly used to construct new type abstractions in formal verification. In such cases, one often wishes to reuse operations on the representation type for the new type abstraction, but to no avail: the types are not the same. To address these problems, we present a new framework that transports programs via equivalences. Existing transport frameworks are either designed for dependently typed, constructive proof assistants, use univalence, or are restricted to partial quotient types. Our framework (1) is designed for simple type theory, (2) generalises previous approaches working on partial quotient types, and (3) is based on standard mathematical concepts, particularly Galois connections and equivalences. We introduce the notion of partial Galois connections and equivalences and prove their closure properties under (dependent) function relators, (co)datatypes, and compositions. We formalised the framework in Isabelle/HOL and provide a prototype. This is the extended version of"Transport via Partial Galois Connections and Equivalences", 21st Asian Symposium on Programming Languages and Systems, 2023.


title: A Fresh Look at Commutativity: Free Algebraic Structures via Fresh Lists

authors:
Clemens Kupke
Fredrik Nordvall Forsberg
Sean Watters


title: Incorrectness Proofs for Object-Oriented Programs via Subclass Reflection

authors:
Wenhua Li
Quang Loc Le
Yahui Song
Wei-Ngan Chin


title: Types and Semantics for Extensible Data Types

authors:
Cas van der Rest
Casper Bach Poulsen


title: Experimenting with an Intrinsically-Typed Probabilistic Programming Language in Coq

authors:
Ayumu Saito
Reynald Affeldt


title: TorchProbe: Fuzzing Dynamic Deep Learning Compilers

authors:
Qidong Su
Chuqin Geng
Gennady Pekhimenko
Xujie Si


title: What Types Are Needed for Typing Dynamic Objects? A Python-Based Empirical Study

authors:
Ke Sun
Sheng Chen
Meng Wang
Dan Hao


title: Compilation Semantics for a Programming Language with Versions

authors:
Yudai Tanabe
Luthfan Anshar Lubis
Tomoyuki Aotani
Hidehiko Masuhara

abstract: Abstract Programming with versions is a paradigm that allows a program to use multiple versions of a module so that the programmer can selectively use functions from both older and newer versions of a single module. Previous work formalized $$\lambda _{\textrm{VL}}$$ λ VL , a core calculus for programming with versions, but it has not been integrated into practical programming languages. In this paper, we propose VL, a Haskell-subset surface language for $$\lambda _{\textrm{VL}}$$ λ VL along with its compilation method. We formally describe the core part of the VL compiler, which translates from the surface language to the core language by leveraging Girard’s translation, soundly infers the consistent version of expressions along with their types, and generates a multi-version interface by bundling specific-version interfaces. We conduct a case study to show how VL supports practical software evolution scenarios and discuss the method’s scalability.


title: Proofs as Terms, Terms as Graphs

abstract: . Starting from an encoding of untyped λ -terms with sharing, defined using synthetic inference rules based on a focused proof system for Gentzen’s LJ , we introduce the positive λ -calculus, a call-by-value calculus with explicit substitutions. This calculus is closely related to Accattoli and Paolini’s value sub-stitution calculus but has a di ff erent style of reduction rules that provides a good notion of sharing along the reduction. We also propose a graphical representation in order to capture the structural equivalence on terms that can be described using rule permutations. On one hand, this graphical representation provides a way to remove redundancy in the syntax, and on the other hand, it allows implementing basic operations such as substitution and reduction in a straightforward way.


title: Towards a Framework for Developing Verified Assemblers for the ELF Format

authors:
Jinhua Wu
Yuting Wang
Meng Sun
Xiangzhe Xu
Yichen Song

abstract: Abstract Most of the existing work on verified compilation leaves unverified the translation of assembly programs into binary code in object file formats (e.g., the Executable and Linkable Format or ELF). The challenges of developing verified assemblers come from the intrinsic complexities in low-level assembling processes caused by the need to support different computer architectures and their details, such as encoding a large number of instructions and verifying its correctness. We present a framework that overcomes the above challenges. It works as a template which may be instantiated to generate verified assemblers for different architectures targeting ELF object files. For this, it is parameterized over the implementation and verification of architecture-dependent assembling processes through well-defined interfaces. By plugging the architecture-dependent parts into the template, we get complete verified assemblers. To manage the complexity in developing and verifying encoding of instructions, we integrate into our framework the CSLED framework for automatically generating verified instruction encoders and decoders from declarative instruction specifications. To show the effectiveness of our framework, we have applied it to generate verified assemblers for the complete X86 and RISC-V assembly languages in CompCert.


title: Comparing Semantic Frameworks for Dependently-Sorted Algebraic Theories

authors:
Benedikt Ahrens
Peter LeFanu Lumsdaine
Paige Randall North

abstract: Algebraic theories with dependency between sorts form the structural core of Martin-L\"of type theory and similar systems. Their denotational semantics are typically studied using categorical techniques; many different categorical structures have been introduced to model them (contextual categories, categories with families, display map categories, etc.) Comparisons of these models are scattered throughout the literature, and a detailed, big-picture analysis of their relationships has been lacking. We aim to provide a clear and comprehensive overview of the relationships between as many such models as possible. Specifically, we take *comprehension categories* as a unifying language and show how almost all established notions of model embed as sub-2-categories (usually full) of the 2-category of comprehension categories.


title: Extending the Quantitative Pattern-Matching Paradigm

authors:
Sandra Alves
Delia Kesner
Miguel Ramos


title: Quantum Bisimilarity Is a Congruence Under Physically Admissible Schedulers

authors:
Lorenzo Ceragioli
Fabio Gadducci
Giuseppe Lomurno
Gabriele Tedeschi


title: A Formal Verification Framework for Tezos Smart Contracts Based on Symbolic Execution

authors:
Thi Thu Ha Doan
Peter Thiemann


title: Non-deterministic, Probabilistic, and Quantum Effects Through the Lens of Event Structures

authors:
Vítor Fernandes
Marc de Visme
Benoît Valiron


title: Hybrid Verification of Declarative Programs with Arithmetic Non-fail Conditions


title: Quantum Programming Without the Quantum Physics

abstract: Abstract We propose a quantum programming paradigm where all data are familiar classical data, and the only non-classical element is a random number generator that can return results with negative probability. Currently, the vast majority of quantum programming languages instead work with quantum data types made up of qubits. The description of their behavior relies on heavy linear algebra and many interdependent concepts and intuitions from quantum physics, which takes dedicated study to understand. We demonstrate that the proposed view of quantum programming explains its central concepts and constraints in more accessible, computationally relevant terms. This is achieved by systematically reducing everything to the existence of that negative-probability random generator, avoiding mention of advanced physics. This makes quantum programming more accessible to programmers without a deep background in physics or linear algebra. The bulk of this paper is written with such an audience in mind. As a working vehicle, we lay out a simple quantum programming language under this paradigm, showing that not only can it express all quantum algorithms, it also naturally captures the semantics of measurement without ever mentioning qubits or collapse.


title: Mode-based Reduction from Validity Checking of Fixpoint Logic Formulas to Test-Friendly Reachability Problem

authors:
Hiroyuki Katsura
Naoki Kobayashi
Ken Sakayori
Ryosuke Sato


title: On Computational Indistinguishability and Logical Relations

authors:
Ugo Dal Lago
Zeinab Galal
Giulia Giusti


title: Relative Completeness of Incorrectness Separation Logic

authors:
Yeonseok Lee
Koji Nakazawa

abstract: Abstract Incorrectness Separation Logic (ISL) is a proof system that is tailored specifically to resolve problems of under-approximation in programs that manipulate heaps, and it primarily focuses on bug detection. This approach is different from the over-approximation methods that are used in traditional logics such as Hoare Logic or Separation Logic. Although the soundness of ISL has been established, its completeness remains unproven. In this study, we establish relative completeness by leveraging the expressiveness of the weakest postconditions; expressiveness is a factor that is critical to demonstrating relative completeness in Reverse Hoare Logic. In our ISL framework, we allow for infinite disjunctions in disjunctive normal forms, where each clause comprises finite symbolic heaps with existential quantifiers. To compute the weakest postconditions in ISL, we introduce a canonicalization that includes variable aliasing.


title: Building a Correct-by-Construction Type Checker for a Dependently Typed Core Language

authors:
Bohdan Liesnikov
Jesper Cockx


title: Generic Reasoning of the Locally Nameless Representation

authors:
Yicheng Ni
Yuting Wang


title: Random-Access Lists, from EE to FP

authors:
Titouan Quennet
Pierre-Évariste Dagand


title: Effective Search Space Pruning for Testing Deep Neural Networks

authors:
Bala Rangayah
Eugene Sng
Minh-Thai Trinh


title: Efficiently Adapting Stateless Model Checking for C11/C++11 to Mixed-Size Accesses

authors:
Shigeyuki Sato
Taiyo Mizuhashi
Genki Kimura
Kenjiro Taura

abstract: Abstract Stateless model checking (SMC) is crucial for productivity in verified concurrent programming, and its recent developments for C/C++ and weak memory models are remarkable. The state-of-the-art SMC for C, GenMC, efficiently verifies C programs based on C11 atomics and pthreads. However, it does not support mixed-size accesses, accesses to the same memory region with different-sized types, even though they are ubiquitous in C/C++, particularly the code for memory management. As a result, GenMC does not work for C/C++ programs containing memory management. To resolve this problem, we develop a method of adapting GenMC to mixed-size accesses preserving its optimality. We experimentally evaluate the efficiency of our extended implementation of GenMC and its efficacy for memory management programs.


title: OBRA: Oracle-Based, Relational, Algorithmic Type Verification

authors:
Elizaveta Vasilenko
Niki Vazou
Gilles Barthe


title: Explaining Explanations in Probabilistic Logic Programming


title: Type-Based Verification of Connectivity Constraints in Lattice Surgery

authors:
Ryo Wakizaka
Yasunari Suzuki
Atsushi Igarashi

abstract: Abstract Fault-tolerant quantum computation using lattice surgery can be abstracted as operations on graphs, wherein each logical qubit corresponds to a vertex of the graph, and multi-qubit measurements are accomplished by connecting the vertices with paths between them. Operations attempting to connect vertices without a valid path will result in abnormal termination. As the permissible paths may evolve during execution, it is necessary to statically verify that the execution of a quantum program can be completed. This paper introduces a type-based method to statically verify that well-typed programs can be executed without encountering halts induced by surgery operations. Alongside, we present $$\mathcal {Q}_{LS}$$ Q LS , a first-order quantum programming language to formalize the execution model of surgery operations. Furthermore, we provide a type checking algorithm by reducing the type checking problem to the offline dynamic connectivity problem.


title: Checking Consistency of Event-Driven Traces

authors:
Parosh Aziz Abdulla
Mohamed Faouzi Atig
R. Govind
Samuel Grahn
Ramanathan S. Thinniyam


title: Positive Sharing and Abstract Machines

authors:
Beniamino Accattoli
Claudio Sacerdoti Coen
Jui-Hsuan Wu


title: A Formal Foundation for Equational Reasoning on Probabilistic Programs

authors:
Reynald Affeldt
Yoshihiro Ishiguro
Zachary Stone


title: Memory Safety: Uniqueness as Separation

authors:
Pilar Selene Linares-Arévalo
Arthur Azevedo de Amorim
Vincent Jackson
Liam O'Connor
Peter Schachte
Christine Rizkallah


title: Fair Termination for Resource-Aware Active Objects

authors:
Francesco Dagnino
Paola Giannini
Violet Ka I Pun
Ulises Torrella


title: IMALL with a Mixed-State Modality: A Logical Approach to Quantum Computation

authors:
Kinnari Dave
Alejandro Díaz-Caro
Vladimir Zamdzhiev

abstract: We introduce a proof language for Intuitionistic Multiplicative Additive Linear Logic (IMALL), extended with a modality B to capture mixed-state quantum computation. The language supports algebraic constructs such as linear combinations, and embeds pure quantum computations within a mixed-state framework via B, interpreted categorically as a functor from a category of Hilbert Spaces to a category of finite-dimensional C*-algebras. Measurement arises as a definable term, not as a constant, and the system avoids the use of quantum configurations, which are part of the theory of the quantum lambda calculus. Cut-elimination is defined via a composite reduction relation, and shown to be sound with respect to the denotational interpretation. We prove n that any linear map on C 2 can be represented within the system, and illustrate this expressiveness with examples such as quantum teleportation and the quantum switch.


title: A Quantum-Control Lambda-Calculus with Multiple Measurement Bases

authors:
Alejandro Díaz-Caro
Nicolas A. Monzon

abstract: We introduce Lambda-SX, a typed quantum lambda-calculus that supports multiple measurement bases. By tracking duplicability relative to arbitrary bases within the type system, Lambda-SX enables more flexible control and compositional reasoning about measurements. We formalise its syntax, typing rules, subtyping, and operational semantics, and establish its key meta-theoretical properties. This proof-of-concept shows that support for multiple bases can be coherently integrated into the type discipline of quantum programming languages.


title: Reachability is Decidable for ATM-Typable Finitary PCF with Effect Handlers

authors:
Ryunosuke Endo
Tachio Terauchi


title: Decision Procedure for a Theory of String Sequences

authors:
Denghang Hu
Taolue Chen
Philipp Rümmer
Fu Song
Zhilin Wu


title: Performance Optimization of HPC Workloads in Cloud Using AI-Driven Algorithms

authors:
Aman Iftekhar
Rahul Mishra


title: Expressive Power of One-Shot Control Operators and Coroutines

authors:
Kentaro Kobayashi
Yukiyoshi Kameyama


title: ELTC: An End-to-End Large Language Model-Based Tensor Compilation Optimization Framework

authors:
WenBo Ma
Qingzeng Song
Fei Qiao
Yongjiang Xue
Mingze Sun


title: Specification Inference Modulo Oracles for Database-Backed Web Applications

authors:
Nitesh Trivedi
Subhajit Roy


venue: cav

title: Extension of the Karp and Miller Procedure to Lotos Specifications

authors:
Michel Barbeau
Gregor von Bochmann


title: PAPETRI: Environment for the Analysis of Petri Nets

authors:
Gérard Berthelot
Colette Johnen
Laure Petrucci


title: Minimal Model Generation

authors:
Ahmed Bouajjani
Jean-Claude Fernandez
Nicolas Halbwachs


title: Formal Verification of Digital Circuits Using Symbolic Ternary System Models

authors:
Randal E. Bryant
Carl-Johan H. Seger


title: Verifying Liveness Properties by Verifying Safety Properties


title: A Proof Lattice-Based Technique for Analyzing Liveness of Resource Controllers

authors:
Ugo A. Buy
Robert Moll


title: The Use of Model Checking in ATPG for Sequential Circuits

authors:
Paolo Camurati
Marco Gilli
Paolo Prinetto
Matteo Sonza Reorda


title: Computer Assistance for Program Refinement

authors:
David A. Carrington
Kenneth Arthur Robinson


title: Temporal Logic Model Checking: Two Techniques for Avoiding the State Explosion Problem


title: On Automatically Explaining Bisimulation Inequivalence


title: Verifying Temporal Properties of Sequential Machines Without Building their State Diagrams

authors:
Olivier Coudert
Jean Christophe Madre
Christian Berthet


title: Memory Efficient Algorithms for the Verification of Temporal Properties

authors:
Costas Courcoubetis
Moshe Y. Vardi
Pierre Wolper
Mihalis Yannakakis


title: Quantitative Temporal Reasoning

authors:
E. Allen Emerson
Aloysius K. Mok
A. Prasad Sistla
Jai Srinivasan


title: Automatic Verification of Extensions of Hardware Descriptions


title: Using Partial Orders to Improve Automatic Verification Methods


title: Task-Driven Supervisory Control of Discrete Event Systems

authors:
Christian H. Golaszewski
Robert P. Kurshan


title: Compositional Minimization of Finite State Systems

authors:
Susanne Graf
Bernhard Steffen


title: Branching Time Regular Temporal Logic for Model Checking with Linear Time Complexity

authors:
Kiyoharu Hamaguchi
Hiromi Hiraishi
Shuzo Yajima


title: Vectorized Model Checking for Computation Tree Logic

authors:
Hiromi Hiraishi
Shintaro Meki
Kiyoharu Hamaguchi


title: Using Optimal Simulations to Reduce Reachability Graphs

authors:
Ryszard Janicki
Maciej Koutny


title: An Algebra for Delay-Insensitive Circuits

authors:
Mark B. Josephs
Jan Tijmen Udding


title: A Context Dependent Equivalence Relation Between Kripke Structures


title: On Using Protean To Verify ISO FTAM Protocol

authors:
Richard Lai
Ken R. Parker
Tharam S. Dillon


title: Automated RTL Verification Based on Predicate Calculus


title: Compositional Design and Verification of Communication Protocols, Using Labelled Petri Nets

authors:
Jean Christophe Lloret
Pierre Azéma
François Vernadat


title: Verification of a Multiprocessor Cache Protocol Using Simulation Relations and Higher-Order Logic

authors:
Paul Loewenstein
David L. Dill


title: Finiteness Conditions and Structural Construction of Automata for All Process Algebras

authors:
Eric Madelaine
Didier Vergamini


title: Program Verification by Symbolic Execution of Hyperfinite Ideal Machines

authors:
James M. Morris
Mark Howard


title: A Data Path Verifier for Register Transfer Level Using Temporal Logic Language Tokio

authors:
Hiroshi Nakamura
Yuji Kukimoto
Masahiro Fujita
Hidehiko Tanaka


title: Issues Arising in the Analysis of L.0


title: A Unified Approach to the Deadlock Detection Problem in Networks of Communicating Finite State Machines

authors:
Wuxu Peng
S. Purushothaman


title: Introduction to a Computational Theory and Implementation of Sequential Hardware Equivalence


title: Using Partial-Order Semantics to Avoid the State Explosion Problem in Asynchronous Systems

authors:
David K. Probst
Hon Fung Li


title: Auto/Autograph

authors:
Valérie Roy
Robert de Simone


title: The Modular Framework of Computer-Aided Verification

authors:
Gil Shurek
Orna Grumberg


title: A Stubborn Attack On State Explosion


title: Synthesizing Processes and Schedulers from Temporal Specifications

authors:
Howard Wong-Toi
David L. Dill


title: The Algebraic Feedback Product of Automata


title: Compositional Checking of Satisfaction

authors:
Henrik Reif Andersen
Glynn Winskel


title: Integer Programming in the Analysis of Concurrent Systems

authors:
George S. Avrunin
Ugo A. Buy
James C. Corbett


title: The Lotos Model of a Fault Protected System and its Verification Using a Petri Net Based Approach

authors:
Michel Barbeau
Gregor von Bochmann


title: Mechanically Checked Proofs of Kernel Specification

authors:
William R. Bevier
Jørgen F. Søgaard-Andersen


title: From Data Structure to Process Structure


title: Efficient Algorithms for Verification of Equivalences for Probabilistic Processes

authors:
Linda Christoff
Ivan Christoff


title: A Linear-Time Model-Checking Algorithm for the Alternation-Free Modal Mu-Calculus

authors:
Rance Cleaveland
Bernhard Steffen


title: Minimum and Maximum Delay Problems in Real-Time Systems


title: An Algebra of Boolean Processes

authors:
Costas Courcoubetis
Susanne Graf
Joseph Sifakis


title: Checking for Language Inclusion Using Simulation Preorders

authors:
David L. Dill
Alan J. Hu
Howard Wong-Toi


title: Generating BDDs for Symbolic Model Checking in CCS

authors:
Reinhard Enders
Thomas Filkorn
Dirk Taubner


title: Complexity Results for POMSET Languages

authors:
Joan Feigenbaum
Jeremy A. Kahn
Carsten Lund


title: "On the Fly" Verification of Behavioural Equivalences and Preorders

authors:
Jean-Claude Fernandez
Laurent Mounier


title: Functional Extension of Symbolic Model Checking


title: Avoiding State Exposion by Composition of Minimal Covering Graphs

authors:
Alain Finkel
Laure Petrucci


title: A Semantic Driven Method to Check the Finiteness of CCS Processes

authors:
Nicoletta De Francesco
Paola Inverardi


title: Verifying Properties of HMS Machine Specifications of Real-Time Systems

authors:
Armen Gabrielian
R. Iyer


title: A Top Down Approach to the Formal Specification of SCI Cache Coherence

authors:
Stein Gjessing
Stein Krogdahl
Ellen Munthe-Kaas


title: Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties

authors:
Patrice Godefroid
Pierre Wolper


title: Mechanically Verifying Safety and Liveness Properties of Delay Insensitive Circuits


title: Formal Verification of Speed-Dependent Asynchronous Cicuits Using Symbolic Model Checking of branching Time Regular Temporal Logic

authors:
Kiyoharu Hamaguchi
Hiromi Hiraishi
Shuzo Yajima


title: Vectorized Symbolic Model Checking of Computation Tree Logic for Sequential Machine Verification

authors:
Hiromi Hiraishi
Kiyoharu Hamaguchi
Hiroyuki Ochi
Shuzo Yajima


title: Deciding Properties of Regular Real Time Processes

authors:
Uno Holmer
Kim Guldstrand Larsen
Wang Yi


title: Silence is Golden: Branching Bisimilarity is Decidable for Context-Free Processes


title: Bounded-memory Algorithms for Verification On-the-fly

authors:
Claude Jard
Thierry Jéron


title: A Linear Time Process Algebra


title: The Concurrency Workbench with Priorities


title: An Automata Theoretic Approach to Temporal Logic


title: Computing Distinguishing Formulas for Branching Bisimulation


title: Comparing Generic State Machines

authors:
Michel Langevin
Eduard Cerny


title: PAM: A Process Algebra Manipulator


title: An Automated Proof Technique for Finite-State Machine Equivalence

authors:
Wenbo Mao
George J. Milne


title: A Proof Assistant for PSF

authors:
Sjouke Mauw
Gert J. Veltink


title: Using the HOL Prove Assistant for proving the Correctness of term Rewriting Rules reducing Terms of Sequential Behavior


title: Mechanizing a Proof by Induction of Process Algebrs Specifications in Higher Order Logic


title: An Action Based Framework for Verifying Logical and Behavioural Properties of Concurrent Systems

authors:
Rocco De Nicola
Alessandro Fantechi
Stefania Gnesi
Gioia Ristori


title: An Overview and Synthesis on Timed Process Algebras

authors:
Xavier Nicollin
Joseph Sifakis


title: Partial-Order Model Checking: A Guide for the Perplexed

authors:
David K. Probst
Hon Fung Li


title: Error Diagnosis in Finite Communicating Systems


title: Automating Most Parts of Hardware Proofs in HOL

authors:
Klaus Schneider
Ramayya Kumar
Thomas Kropf


title: A Two-Level Formal Verification Methodology using HOL and COSMOS

authors:
Carl-Johan H. Seger
Jeffrey J. Joyce


title: Automatic Temporal Verification of Buffer Systems

authors:
A. Prasad Sistla
Lenore D. Zuck


title: Taming Infinite State Spaces


title: Temporal Precondition Verification of Design Transformations

authors:
Ranga Vemuri
Anuradha Sridhar


title: Verifying a Logic Synthesis Tool in Nuprl: A Case Study in Software Verification

authors:
Mark D. Aagaard
Miriam Leeser


title: Timing Verification by Successive Approximation

authors:
Rajeev Alur
Alon Itai
Robert P. Kurshan
Mihalis Yannakakis


title: A Verification Strategy for Timing-Constrained Systems

authors:
Felice Balarin
Alberto L. Sangiovanni-Vincentelli


title: Property Preserving Simulations

authors:
Saddek Bensalem
Ahmed Bouajjani
Claire Loiseaux
Joseph Sifakis


title: Symbolic Bisimulation Minimisation

authors:
Amar Bouali
Robert de Simone


title: A Proof Assistant for Symbolic Model-Checking


title: A Case Study in Safety-Critical Design


title: Generating Diagnostic Information for Behavioral Preorders

authors:
Ufuk Celikkan
Rance Cleaveland


title: Decidability of Bisimulation Equivalences for Parallel Timer Processes


title: Faster Model Checking for the Modal Mu-Calculus

authors:
Rance Cleaveland
Marion Klein
Bernhard Steffen


title: Verifying General Safety and Liveness Propterties with Integer Programming


title: Verification with Real-Time COSPAN

authors:
Costas Courcoubetis
David L. Dill
Magda Chatzaki
Panagiotis Tzounakis


title: Modular Abstractions for Verifying Real-Time Distributed Systems

authors:
Hana De-Leon
Orna Grumberg


title: Mechanical Verification of Concurrent Systems with TLA

authors:
Urban Engberg
Peter Grønning
Leslie Lamport


title: Verification in Process Algebra of the Distributed Control of Track Vehicles - A Case Study

authors:
Siegfried Fischer
Andreas Scholz
Dirk Taubner


title: State-Space Caching Revisited

authors:
Patrice Godefroid
Gerard J. Holzmann
Didier Pirottin


title: Design Verification of a Microprocessor Using Branching Time Regular Temporal Logic

authors:
Kiyoharu Hamaguchi
Hiromi Hiraishi
Shuzo Yajima


title: A Verification Procedure via Invariant for Extended Communicating Finite-State Machines

authors:
Masahiro Higuchi
Osamu Shirakawa
Hiroyuki Seki
Mamoru Fujii
Tadao Kasami


title: Efficient omega-Regular Language Containment

authors:
Ramin Hojati
Hervé J. Touati
Robert P. Kurshan
Robert K. Brayton


title: Higher-Level Specification and Verification with BDDs

authors:
Alan J. Hu
David L. Dill
Andreas J. Drexler
C. Han Yang


title: Towards a Verification Technique for Large Synchronous Circuits

authors:
Prabhat Jain
Prabhakar Kudva
Ganesh Gopalakrishnan


title: Compositional Model Checking for Linear-Time Temporal Logic


title: Computer-Hindered Verification (Humans Can Do It Too)


title: Efficient Local Correctness Checking


title: Tableau Recycling


title: Using Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits


title: Crocos: An Integrated Environment for Interactive Verification of SDL Specifications

authors:
Dominique Méry
Abdelillah Mokkedem


title: Layering Techniques for Development of Parallel Systems

authors:
Mannes Poel
Job Zwiers


title: Verifying Timed Behavior Automata with Nonbinary Delay Constraints

authors:
David K. Probst
Hon Fung Li


title: Model-Checking for Real-Time Systems Specified in Lotos

authors:
Nathalie Rico
Gregor von Bochmann
Omar Cherkaoui


title: Automatic Reduction in CTL Compositional Model Checking

authors:
Thomas R. Shiple
Massimiliano Chiodo
Alberto L. Sangiovanni-Vincentelli
Robert K. Brayton


title: Using a Theorem Prover for Reasoning about Concurrent Algorithms

authors:
Joakim von Wright
Thomas Långbacka


title: Computing Accumulated Delays in Real-time Systems

authors:
Rajeev Alur
Costas Courcoubetis
Thomas A. Henzinger


title: An Iterative Approach to Language Containment

authors:
Felice Balarin
Alberto L. Sangiovanni-Vincentelli


title: Logic Synthesis and Design Verification


title: Functionality Decomposition by Compositional Correstness Preserving Transformation

authors:
Ed Brinksma
Rom Langerak
Peter Broekroelofs


title: Timed Modal Specification - Theory and Tools

authors:
Karlis Cerans
Jens Chr. Godskesen
Kim Guldstrand Larsen


title: Exploiting Symmetry In Temporal Logic Model Checking

authors:
Edmund M. Clarke
Thomas Filkorn
Somesh Jha


title: Verification of timing Properties of VHDL

authors:
Costas Courcoubetis
Werner Damm
Bernhard Josko


title: Generation of Reduced Models for Checking Fragments of CTL

authors:
Dennis Dams
Orna Grumberg
Rob Gerth


title: On Model-Checking for Fragments of µ-Calculus

authors:
E. Allen Emerson
Charanjit S. Jutla
A. Prasad Sistla


title: Symmetry and Model Checking

authors:
E. Allen Emerson
A. Prasad Sistla


title: Symbolic Equivalence Checking

authors:
Jean-Claude Fernandez
Alain Kerbrat
Laurent Mounier


title: Refining Dependencies Improves Partial-Order Verification Methods (Extended Abstract)

authors:
Patrice Godefroid
Didier Pirottin


title: A Verifier and Timing Analyser for Simple Imperative Programs (Abstract)


title: A Tool for Symbolic Program Verification and Abstration

authors:
Susanne Graf
Claire Loiseaux


title: Parametric Circuit Representation Using Inductive Boolean Functions

authors:
Aarti Gupta
Allan L. Fisher


title: Delay Analysis in Synchronous Programs


title: A Modal Logic for Message passing Processes (Extended Abstract)

authors:
Matthew Hennessy
Xinxin Liu


title: BDD-Based Debugging Of Design Using Language Containment and Fair CTL

authors:
Ramin Hojati
Robert K. Brayton
Robert P. Kurshan


title: Efficient Verification with BDDs using Implicitly Conjoined Invariants

authors:
Alan J. Hu
David L. Dill


title: Combining Model Checking and Theorem Proving to Verify Parallel Processes


title: Verifying Quantitative Real-Time Properties of Synchronous Programs

authors:
Martin Jourdan
Florence Maraninchi
Alfredo Olivero


title: A Decision Algorithm for Full Propositional Temporal Logic

authors:
Yonit Kesten
Zohar Manna
Hugh McGuire
Amir Pnueli


title: Reachability and Recurrence in Extended Finite State Machines: Modular Vector Addition Systems


title: Verification of a Multiplier: 64 Bits and Beyond

authors:
Robert P. Kurshan
Leslie Lamport


title: A Structural Linearization Principle for Processes

authors:
Robert P. Kurshan
Michael Merritt
Ariel Orda
Sonia R. Sachs


title: A Graphical Interval Logic Toolset for Verifying Concurrent Systems

authors:
George Kutty
Y. S. Ramakrishna
Louise E. Moser
Laura K. Dillon
P. M. Melliar-Smith


title: Alternating RQ Timed Automata

authors:
William K. C. Lam
Robert K. Brayton


title: The Formal Verification of an Algorithm for Interactive Consistency under a Hybrid Fault Model

authors:
Patrick Lincoln
John M. Rushby


title: Reachability Analysis of Planar Multi-limear Systems

authors:
Oded Maler
Amir Pnueli


title: All from One, One for All: on Model Checking Using Representatives


title: Verifying Timed Behavior Automata with Input/Output Critical Races

authors:
David K. Probst
Hon Fung Li


title: Automatic Generation of Network Invariants for the Verification of Iterative Sequential Systems

authors:
June-Kyung Rho
Fabio Somenzi


title: Verification of Real-Time Systems Using PVS


title: Computer-Assisted Simulation Proofs

authors:
Jørgen F. Søgaard-Andersen
Stephen J. Garland
John V. Guttag
Nancy A. Lynch
Anna Pogosyants


title: On-the-Fly Verification with Stubborn Sets


title: Protocol Design for an Automated Highway System (Abstract)


title: A Mechanically Verified Application for a Mechanically Verified Environment


title: Reliable Hashing without Collosion Detection

authors:
Pierre Wolper
Denis Leroy


title: An Efficient Algorithm for Minimizing Real-time Transition Systems

authors:
Mihalis Yannakakis
David Lee


title: Efficient Verification of Parallel Real-Time Systems

authors:
Tomohiro Yoneda
Atsufumi Shibayama
Bernd-Holger Schlingloff
Edmund M. Clarke


title: A Determinizable Class of Timed Automata

authors:
Rajeev Alur
Limor Fix
Thomas A. Henzinger


title: Realizability and Synthesis of Reactive Modules

authors:
Anuchit Anuchitanukul
Zohar Manna


title: Formula-Dependent Equivalence for Compositional CTL Model Checking

authors:
Adnan Aziz
Thomas R. Shiple
Vigyan Singhal


title: On the Automatic Computation of Network Invariants

authors:
Felice Balarin
Alberto L. Sangiovanni-Vincentelli


title: Methodology and System for Practical Formal Verification of Reactive Hardware

authors:
Ilan Beer
Shoham Ben-David
Daniel Geist
Raanan Gewirtzman
Michael Yoeli


title: An Automata-Theoretic Approach to Branching-Time Model Checking (Extended Abstract)

authors:
Orna Bernholtz
Moshe Y. Vardi
Pierre Wolper


title: Symbolic Verification with Periodic Sets

authors:
Bernard Boigelot
Pierre Wolper


title: Verification of Context-Free Timed Systems Using Linear Hybrid Observers

authors:
Ahmed Bouajjani
Rachid Echahed
Riadh Robbana


title: Automatic verification of Pipelined Microprocessor Control

authors:
Jerry R. Burch
David L. Dill


title: Another Look at LTL Model Checking

authors:
Edmund M. Clarke
Orna Grumberg
Kiyoharu Hamaguchi


title: Performance Improvement of State Space Exploration by Regular & Diffrential Hashing Functions

authors:
Bernard Cousin
Jean-Michel Hélary


title: Ground Temporal Logic: A Logic for Hardware Verification

authors:
David Cyrluk
Paliath Narendran


title: Model Checking Using Adaptive State and Data Abstraction

authors:
Dennis Dams
Rob Gerth
Gert Döhmen
Ronald Herrmann
Peter Kelb
Hergen Pargmann


title: Efficient Model Checking by Automated Ordering of Transition Relation Partitions

authors:
Daniel Geist
Ilan Beer


title: Real-Time System Verification using P/T Nets

authors:
Roberto Gorrieri
Glauco Siliprandi


title: Verification of a Distributed Cache Memory by Using Abstractions


title: Composing Symbolic Trajectory Evaluation Results

authors:
Scott Hazelhurst
Carl-Johan H. Seger


title: Improving Language Containment Using Fairness Graphs

authors:
Ramin Hojati
Robert B. Mueller-Thuns
Robert K. Brayton


title: Model Checking of macro Processes


title: Models Whose Checks Don't Explode


title: Criteria for the Simple Path Property in Timed Automata

authors:
William K. C. Lam
Robert K. Brayton


title: A Parallel Algorithm for Relational Coarsest Partition Problems and Its Implementation

authors:
Insup Lee
Sanguthevar Rajasekaran


title: An Improved Algorithm for the Evaluation of Fixpoint Expressions

authors:
David E. Long
Anca Browne
Edmund M. Clarke
Somesh Jha
Wilfredo R. Marrero


title: Beyond Model Checking


title: Suspension Automata: A Decidable Class of Hybrid Automata

authors:
Jennifer McManis
Pravin Varaiya


title: Hierarchical Representations of Discrete Functions, with Application to Model Checking


title: On the Random Walk Method for Protocol Testing

authors:
Milena Mihail
Christos H. Papadimitriou


title: Modeling and Verification of a Real Life Protocol Using Symbolic Model Checking

authors:
Vivek G. Naik
A. Prasad Sistla


title: Using Abstractions for the Verification of Linear Hybrid Systems

authors:
Alfredo Olivero
Joseph Sifakis
Sergio Yovine


title: Combining Partial Order Reductions with On-the-fly Model-Checking


title: Decidability of Hybrid Systems with Rectangular Differential Inclusion

authors:
Anuj Puri
Pravin Varaiya


title: Automatic Verification of Timed Circuits

authors:
Tomas Rokicki
Chris J. Myers


title: A Hybrid Model for Reasoning about Composed Hardware Systems


title: Compositional Semantics of ESTEREL and Verification by Compositional Reductions

authors:
Robert de Simone
Annie Ressouche


title: The Verifiacation Problem for Safe Replaceability

authors:
Vigyan Singhal
Carl Pixley


title: Incremental Model Checking in the Modal Mu-Calculus

authors:
Oleg Sokolsky
Scott A. Smolka


title: The Mobility Workbench - A Tool for the pi-Calculus

authors:
Björn Victor
Faron Moller


title: The Completeness of a Hardware Inference System

authors:
Zheng Zhu
Carl-Johan H. Seger


title: Local Liveness for Compositional Modeling of Fair Reactive Systems

authors:
Rajeev Alur
Thomas A. Henzinger


title: Efficient Checking of Behavioural Relations and Modal Assertions using Fixed-Point Inversion

authors:
Henrik Reif Andersen
Bart Vergauwen


title: Supervisory Control of Finite State Machines

authors:
Adnan Aziz
Felice Balarin
Robert K. Brayton
Marika Domenica Di Benedetto
Alexander Saldanha


title: It Usually Works: The Temporal Logic of Stochastic Systems

authors:
Adnan Aziz
Vigyan Singhal
Felice Balarin


title: Hardware Verification using Monadic Second-Order Logic

authors:
David A. Basin
Nils Klarlund

abstract: We show how the second-order monadic theory of strings can be used to specify hardware components and their behavior. This logic admits a decision procedure and counter-model generator based on canonical automata for formulas. We have used a system implementing these concepts to verify, or find errors in, a number of circuits proposed in the literature. The techniques we use make it easier to identify regularity in circuits, including those that are parameterized or have parameterized behavioral specifications. Our proofs are semantic and do not require lemmas or induction as would be needed when employing a conventional theory of strings as a recursive data type.


title: Global rebuilding of OBDDs Avoiding Memory Requirement Maxima

authors:
Jochen Bern
Christoph Meinel
Anna Slobodová


title: From Duration Calculus To Linear Hybrid Automata

authors:
Ahmed Bouajjani
Yassine Lakhnech
Riadh Robbana


title: Verifying omega-Regular Properties for a Subclass of Linear Hybrid Systems

authors:
Ahmed Bouajjani
Riadh Robbana


title: Multipliers and Dividers: Insights on Arithmetic Circuits Verification (Extended Abstract)


title: Compositional and Inductive Semantic Definitions in Fixpoint, Equational, Constraint, Closure-condition, Rule-based and Game-Theoretic Form

authors:
Patrick Cousot
Radhia Cousot


title: Verification of Real-Time Systems by Successive Over and Under Approximation

authors:
David L. Dill
Howard Wong-Toi


title: Model Checking for Infinite State Systems Using Data Abstraction, Assumption-Commitment Style reasoning and Theorem Proving

authors:
Jürgen Dingel
Thomas Filkorn


title: Generating BDD Models for Process Algebra Terms

authors:
Ashvin Dsouza
Bard Bloom


title: Using Formal Verification/Analysis Methods on the Critical Path in System Design: A Case Study

authors:
Ásgeir Th. Eiríksson
Kenneth L. McMillan


title: Methods for Mu-calculus Model Checking: A Tutorial (Abstract)


title: Utilizing Symmetry when Model Checking under Fairness Assumptions: An Automata-theoretic Approach

authors:
E. Allen Emerson
A. Prasad Sistla


title: On the Model Checking Problem for Branching Time Logics and Basic Parallel Processes

authors:
Javier Esparza
Astrid Kiehn


title: Interactively Verifying a Simple Real-time Scheduler

authors:
Colin J. Fidge
Peter Kearney
Mark Utting


title: CAVEAT: Technique and Tool for Computer Aided VErification And Transformation

authors:
E. Pascal Gribomont
Didier Rossetto


title: Algorithmic Analysis of Nonlinear Hybrid Systems

authors:
Thomas A. Henzinger
Pei-Hsin Ho


title: Automated Analysis of an Audio Control Protocol

authors:
Pei-Hsin Ho
Howard Wong-Toi


title: Automatic Datapath Abstraction In Hardware Systems

authors:
Ramin Hojati
Robert K. Brayton


title: Efficient Timing Analysis of a Class of Petri Nets

authors:
Henrik Hulgaard
Steven M. Burns


title: Safety Property Verification of ESTEREL Programs and Applications to Telecommunications Software

authors:
Lalita Jategaonkar Jagadeesan
Carlos Puchol
James Von Olnhausen


title: Verifying Safety Properties of a Class of Infinite-State Distributed Algorithms

authors:
Bengt Jonsson
Lars Kempe


title: The Rabin Index and Chain Automata, with Applications to Automatas and Games

authors:
Sriram C. Krishnan
Anuj Puri
Robert K. Brayton
Pravin Varaiya


title: Augmenting Branching Temporal Logics with Existential Quantification over Atomic Propositions


title: Modelling Asynchrony with a Synchronous Model

authors:
Robert P. Kurshan
Michael Merritt
Ariel Orda
Sonia R. Sachs


title: On Polynomial-Size Programs Winning Finite-State Games


title: Trace Theoretic Verification of Asynchronous Circuits Using Unfoldings


title: An Integration of Model Checking with Automated Proof Checking

authors:
S. Rajan
Natarajan Shankar
Mandayam K. Srivas


title: Toupie = µ-Calculus + Constraints


title: Local Model Checking for Real-Time Systems (Extended Abstract)

authors:
Oleg Sokolsky
Scott A. Smolka


title: An Automata-Theoretic Approach to Fair Realizability and Synthesis


title: Temporal Verification by Diagram Transformations

authors:
Luca de Alfaro
Zohar Manna


title: Marella: A Tool for Simulation and Verification

authors:
Dominique Ambroise
Brigitte Rozoy


title: MDG Tools for the Verification of RTL Designs

authors:
K. D. Anon
N. Boulerice
Eduard Cerny
Francisco Corella
Michel Langevin
Xiaoyu Song
Sofiène Tahar
Ying Xu
Zijian Zhou


title: Symbolic Model Checking Using Algebraic Geometry


title: Verifying Continuous Time Markov Chains

authors:
Adnan Aziz
Kumud Sanwal
Vigyan Singhal
Robert K. Brayton


title: Polynomial Time Algorithms for Testing Probabilistic Bisimulation and Simulation


title: Verification of an Audio Protocol with Bus Collision Using UPPAAL

authors:
Johan Bengtsson
W. O. David Griffioen
Kåre J. Kristoffersen
Kim Guldstrand Larsen
Fredrik Larsson
Paul Pettersson
Wang Yi


title: Powerful Techniques for the Automatic Generation of Invariants

authors:
Saddek Bensalem
Yassine Lakhnech
Hassen Saïdi


title: Automated Verification by Induction with Associative-Commutative Operators

authors:
Narjes Berregeb
Adel Bouhoula
Michaël Rusinowitch


title: STeP: Deductive-Algorithmic Verification of Reactive and Real-Time Systems

authors:
Nikolaj S. Bjørner
Anca Browne
Edward Y. Chang
Michael Colón
Arjun Kapur
Zohar Manna
Henny Sipma
Tomás E. Uribe


title: Symbolic Verification of Communication Protocols with Infinite State Spaces Using QDDs (Extended Abstract)

authors:
Bernard Boigelot
Patrice Godefroid


title: The FC2TOOLS Set

authors:
Amar Bouali
Annie Ressouche
Valérie Roy
Robert de Simone


title: VIS: A System for Verification and Synthesis

authors:
Robert K. Brayton
Gary D. Hachtel
Alberto L. Sangiovanni-Vincentelli
Fabio Somenzi
Adnan Aziz
Szu-Tsung Cheng
Stephen A. Edwards
Sunil P. Khatri
Yuji Kukimoto
Abelardo Pardo
Shaz Qadeer
Rajeev K. Ranjan
Shaker Sarwary
Thomas R. Shiple
Gitanjali Swamy
Tiziano Villa


title: Selective Quantitative Analysis and Interval Model Checking: Verifying Different Facets of a System

authors:
Sérgio Vale Aguiar Campos
Orna Grumberg


title: Verification by Behaviour Abstraction - A Case Study of Service Interaction Detection in Intelligent Telephone Networks

authors:
Carla Capellmann
Ralph Demant
Farhad Fatahi-Vanani
Rafael Galvez-Estrada
Ulrich Nitsche
Peter Ochsenschläger


title: XVERSA: An Integrated Graphical and Textual Toolset for the Specification and Analysis of Resource-Bound Real-Time Systems

authors:
Duncan Clarke
Hanêne Ben-Abdallah
Insup Lee
Hong-liang Xie
Oleg Sokolsky


title: Verifying the SRT Division Algorithm Using Theorem Proving Techniques

authors:
Edmund M. Clarke
Steven M. German
Xudong Zhao


title: Symbolic Model Checking

authors:
Edmund M. Clarke
Kenneth L. McMillan
Sérgio Vale Aguiar Campos
Vasiliki Hartonas-Garmhausen


title: The Concurrency Factory: A Development Environment for Concurrent Systems

authors:
Rance Cleaveland
Philip M. Lewis
Scott A. Smolka
Oleg Sokolsky


title: The NCSU Concurrency Workbench

authors:
Rance Cleaveland
Steve Sims


title: The Murphi Verification System


title: Automatic Verification of Parameterized Synchronous Systems (Extended Abstract)

authors:
E. Allen Emerson
Kedar S. Namjoshi


title: CADP - A Protocol Validation and Verification Toolbox

authors:
Jean-Claude Fernandez
Hubert Garavel
Alain Kerbrat
Laurent Mounier
Radu Mateescu
Mihaela Sighireanu


title: Using On-The-Fly Verification Techniques for the Generation of test Suites

authors:
Jean-Claude Fernandez
Claude Jard
Thierry Jéron
César Viho


title: Verification of Arithmetic Circuits by Comparing Two Similar Circuits


title: Verifying the Safety of a Practical Concurrent Garbage Collector


title: Verifying Invariants Using theorem Proving

authors:
Susanne Graf
Hassen Saïdi


title: Verifying Safety Properties of Differential Equations


title: Atomicity Refinement and Trace Reduction Theorems


title: The State of SPIN

authors:
Gerard J. Holzmann
Doron A. Peled


title: Verifying Systems with Replicated Components in Murphi

authors:
C. Norris Ip
David L. Dill


title: Mechanically Verifying a Family of Multiplier Circuits

authors:
Deepak Kapur
Mahadevan Subramaniam


title: Verification Support Environment

authors:
Frank A. Koch
Markus Ullmann
Stefan Wittmann


title: Module Checking

authors:
Orna Kupferman
Moshe Y. Vardi


title: Verification of Fair Transisiton Systems


title: A Conjunctively Decomposed Boolean Representation for Symbolic Model Checking


title: EVP: Integration of FDTs for the Analysis and Verification of Communication Protocols

authors:
Pedro Merino
José M. Troya


title: Saving Space by Fully Exploiting Invisible Transitions

authors:
Hillel Miller
Shmuel Katz


title: The Real-Time Graphical Interval Logic Toolset

authors:
Louise E. Moser
P. M. Melliar-Smith
Y. S. Ramakrishna
George Kutty
Laura K. Dillon


title: Automatic Translation of Natural Language System Specifications

authors:
Rani Nelken
Nissim Francez


title: PVS: Combining Specification, Proof Checking, and Model Checking

authors:
Sam Owre
S. Rajan
John M. Rushby
Natarajan Shankar
Mandayam K. Srivas


title: Protocol Verification by Aggregation of Distributed Transactions

authors:
Seungjoon Park
David L. Dill


title: A Partition Refinement Algorithm for the pi-Calculus (Extended Abstract)

authors:
Marco Pistore
Davide Sangiorgi


title: A Platform for Combining Deductive with Algorithmic Verification

authors:
Amir Pnueli
Elad Shahar


title: Modular Verification of SRT Division

authors:
Harald Rueß
Natarajan Shankar
Mandayam K. Srivas


title: Automated Deduction and Formal Methods


title: HORNSAT, Model Checking, Verification and games (Extended Abstract)

authors:
Sandeep K. Shukla
Harry B. Hunt III
Daniel J. Rosenkrantz


title: Deductive Model Checking

authors:
Henny Sipma
Tomás E. Uribe
Zohar Manna


title: The METAFrame'95 Environment

authors:
Bernhard Steffen
Tiziana Margaria
Andreas Claßen
Volker Braun


title: Analysis of Timed Systems Based on Time-Abstracting Bisimulation

authors:
Stavros Tripakis
Sergio Yovine


title: Pushdown Processes: Games and Model Checking


title: Partial-Order Reduction in Symbolic State Space Exploration

authors:
Rajeev Alur
Robert K. Brayton
Thomas A. Henzinger
Shaz Qadeer
Sriram K. Rajamani


title: Weak Bisimulation for Fully Probabilistic Processes

authors:
Christel Baier
Holger Hermanns


title: Model Checking in a Microprocessor Design Project

authors:
Geoff Barrett
Anthony McIsaac


title: RuleBase: Model Checking at IBM

authors:
Ilan Beer
Shoham Ben-David
Cindy Eisner
Daniel Geist
Leonid Gluhovsky
Tamir Heyman
Avner Landver
P. Paanah
Yoav Rodeh
G. Ronin
Yaron Wolfsthal


title: Efficient Detection of Vacuity in ACTL Formulaas

authors:
Ilan Beer
Shoham Ben-David
Cindy Eisner
Yoav Rodeh


title: Boolean and 2-adic Numbers Based Techniques for Verifying Synchronous Design


title: µcke - Efficient µ-Calculus Model Checking


title: An Improved Reachability Analysis Method for Strongly Linear Hybrid Systems (Extended Abstract)

authors:
Bernard Boigelot
Louis Bronne
Stéphane Rassart


title: Towards a Mechanization of Cryptographic Protocal Verification


title: The Industrial Success of Verification Tools Based on Stålmarck's Method


title: Some Progress in the Symbolic Verification of Timed Automata

authors:
Marius Bozga
Oded Maler
Amir Pnueli
Sergio Yovine


title: Symbolic Model Checking of Infinite State Systems Using Presburger Arithmetic

authors:
Tevfik Bultan
Richard Gerber
William W. Pugh


title: The Verus Tool: A Quantitative Approach to the Formal Verification of Real-Time Systems

authors:
Sérgio Vale Aguiar Campos
Edmund M. Clarke
Marius Minea


title: Programs with Quasi-Stable Channels are Effectively Recognizable (Extended Abstract)

authors:
Gérard Cécé
Alain Finkel


title: Combining Constraint Solving and Symbolic Model Checking for a Class of a Systems with Non-linear Constraints

authors:
William Chan
Richard J. Anderson
Paul Beame
David Notkin


title: A Provably Correct Embedded Verifier for the Certification of Safety Critical Software

authors:
Alessandro Cimatti
Fausto Giunchiglia
Paolo Pecchiari
Bruno Pietra
Joe Profeta
Dario Romano
Paolo Traverso
Bing Yu


title: An Efficient Decision Procedure for the Theory of Fixed-Sized Bit-Vectors

authors:
David Cyrluk
M. Oliver Möller
Harald Rueß


title: Containing of Regular Languages in Non-Regular Timing Diagram Languages is Decidable


title: VeriSoft: A Tool for the Automatic Analysis of Concurrent Reactive Software


title: Construction of Abstract State Graphs with PVS

authors:
Susanne Graf
Hassen Saïdi


title: The PEP Tool


title: On-the-Fly Model Checking Under Fairness That Exploits Symmetry

authors:
Viktor Gyuris
A. Prasad Sistla


title: Some Thoughts on Statecharts, 13 Years Later


title: HYTECH: A Model Checker for Hybrid Systems

authors:
Thomas A. Henzinger
Pei-Hsin Ho
Howard Wong-Toi


title: Formal Verification of Digital Systems, from ASICs to HW/SW Codesign - a Pragmatic Approach


title: Model Checking and Transitive-Closure Logic

authors:
Neil Immerman
Moshe Y. Vardi


title: Using Compositional Preorders in the Verification of Sliding Window Protocal


title: Automatic Datapath Extraction for Efficient Usage of HDD

authors:
Gila Kamhi
Osnat Weissberg
Limor Fix


title: MOSEL: A Sound and Efficient Tool for M2L(Str)

authors:
Peter Kelb
Tiziana Margaria
Michael Mendler
Claudia Gsottberger


title: Symbolic Model Checking with Rich ssertional Languages

authors:
Yonit Kesten
Oded Maler
Monica Marcus
Amir Pnueli
Elad Shahar


title: An n log n Algorithm for Online BDD Refinement


title: Relaxed Visibility Enhances Partial Order Reduction

authors:
Ilkka Kokkarinen
Doron A. Peled
Antti Valmari


title: Module Checking Revisited

authors:
Orna Kupferman
Moshe Y. Vardi


title: UPPAAL: Status & Developments

authors:
Kim Guldstrand Larsen
Paul Pettersson
Wang Yi


title: TermiLog: A System for Checking Termination of Queries to Logic Programs

authors:
Naomi Lindenstrauss
Yehoshua Sagiv
Alexander Serebrenik


title: Practical Challenges for Industrial Formal Verification Tools


title: A Compositional Rule for Hardware Design Refinement


title: Deadlock Checking Using Net Unfoldings

authors:
Stephan Melzer
Stefan Römer


title: Exploiting Symmetry When Verifying Transitor-Level Circuits by Symbolic Trajectory Evaluation

authors:
Manish Pandey
Randal E. Bryant


title: Automatic Abstraction Techniques for Propositional µ-calculus Model Checking

authors:
Abelardo Pardo
Gary D. Hachtel


title: Efficient Model Checking Using Tabled Resolution

authors:
Y. S. Ramakrishna
C. R. Ramakrishnan
I. V. Ramakrishnan
Scott A. Smolka
Terrance Swift
David Scott Warren


title: Formal Verification - Applications & Case Studies


title: The Invariant Checker: Automated Deductive Verification of Reactive Systems


title: Trace Table Based Approach for Pipeline Microprocessor Verification

authors:
Jun Sawada
Warren A. Hunt Jr.


title: Parametrized Verification of Linear Networks Using Automata as Invariants


title: SMC: A Symmetry Based Model Checker for Verification of Liveness Properties

authors:
A. Prasad Sistla
L. Miliades
Viktor Gyuris


title: Parallelizing the Murphi Verifier

authors:
Ulrich Stern
David L. Dill


title: STARI: A Case Study in Compositional and Hierarchical Timing Verification

authors:
Serdar Tasiran
Robert K. Brayton


title: Verification of a Chemical Process Leak Test Procedure

authors:
Adam L. Turk
Scott T. Probst
Gary J. Powers


title: prod 3.2: An Advanced Tool for Efficient Reachability Analysis

authors:
Kimmo Varpaaniemi
Keijo Heljanko
Johan Lilius


title: Efficient Modeling of Memory Arrays in Symbolic Simulation

authors:
Miroslav N. Velev
Randal E. Bryant
Alok Jain


title: On Combining Formal and Informal Verification

authors:
Jun Yuan
Jian Shen
Jacob A. Abraham
Adnan Aziz


title: On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels

authors:
Parosh Aziz Abdulla
Ahmed Bouajjani
Bengt Jonsson


title: A General Approach to Partial Order Reductions in Symbolic Verification (Extended Abstract)

authors:
Parosh Aziz Abdulla
Bengt Jonsson
Mats Kindahl
Doron A. Peled


title: MOCHA: Modularity in Model Checking

authors:
Rajeev Alur
Thomas A. Henzinger
Freddy Y. C. Mang
Shaz Qadeer
Sriram K. Rajamani
Serdar Tasiran


title: Correctness of the Concurrent Approach to Symbolic Verification of Interleaved Models


title: On-the-Fly Model Checking of RCTL Formulas

authors:
Ilan Beer
Shoham Ben-David
Avner Landver


title: Mechanising BAN Kerberos by the Inductive Method

authors:
Giampaolo Bella
Lawrence C. Paulson


title: Verification of Timed Systems Using POSETs

authors:
Wendy Belluomini
Chris J. Myers


title: Computing Abstractions of Infinite State Systems Compositionally and Automatically

authors:
Saddek Bensalem
Yassine Lakhnech
Sam Owre


title: InVeST: A Tool for the Verification of Invariants


title: Integrating Proof-Based and Model-Checking Techniques for the Formal Verification of Cryptographic Protocols


title: XEVE, an ESTEREL Verification Environment


title: Kronos: A Model-Checking Tool for Real-Time Systems

authors:
Marius Bozga
Conrado Daws
Oded Maler
Alfredo Olivero
Stavros Tripakis
Sergio Yovine


title: Real-Time Verification of Statemate Designs

authors:
Udo Brockmeyer
Gunnar Wittich


title: A Role for Theorem Proving in Multi-Processor Design


title: Verification of Floating-Point Adders

authors:
Yirng-An Chen
Randal E. Bryant


title: Symmetry Reductions in Model Checking

authors:
Edmund M. Clarke
E. Allen Emerson
Somesh Jha
A. Prasad Sistla


title: Generating Finite-State Abstractions of Reactive Systems Using Decision Procedures

authors:
Michael Colón
Tomás E. Uribe


title: Multiple Counters Automata, Safety Analysis and Presburger Arithmetic

authors:
Hubert Comon
Yan Jurski


title: An Experiment in Parallelizing an Application Using Formal Methods

authors:
Raphaël Couturier
Dominique Méry


title: Formal Methods in an Industrial Environment


title: Optikron: A Tool Suite for Enhancing Model-Checking of Real-Time Systems


title: MONA 1.x: New Techniques for WS1S and WS2S

authors:
Jacob Elgaard
Nils Klarlund
Anders Møller


title: Verification of Parameterized Bus Arbitration Protocol

authors:
E. Allen Emerson
Kedar S. Namjoshi


title: Protocol Verification in Nuprl

authors:
Amy P. Felty
Douglas J. Howe
Frank A. Stomp


title: Verifying Mobile Processes in the HAL Environment

authors:
Gian-Luigi Ferrari
Stefania Gnesi
Ugo Montanari
Marco Pistore
Gioia Ristori


title: BDD Based Procedures for a Theory of Equality with Uninterpreted Functions

authors:
Anuj Goel
Khurram Sajid
Hai Zhou
Adnan Aziz
Vigyan Singhal


title: Normed Simulations

authors:
W. O. David Griffioen
Frits W. Vaandrager


title: Synchronous Programming of Reactive Systems


title: Transforming the Theorem Prover into a Digital Design Tool: From Concept Car to Off-Road Vehicle

authors:
David S. Hardin
Matthew Wilding
David A. Greve


title: SCR*: A Toolset for Specifying and Analyzing Software Requirements

authors:
Constance L. Heitmeyer
James Kirby
Bruce G. Labaw
Ramesh Bharadwaj


title: From Pre-historic to Post-modern Symbolic Model Checking

authors:
Thomas A. Henzinger
Orna Kupferman
Shaz Qadeer


title: You Assume, We Guarantee: Methodology and Case Studies

authors:
Thomas A. Henzinger
Shaz Qadeer
Sriram K. Rajamani


title: A Formal Method Experience at Secure Computing Corporation

authors:
John Hoffman
Charlie Payne


title: On Checking Model Checkers

abstract: It has become good practice to expect authors of new model checking algorithms to provide not only rigorous evidence of the algorithms correctness, but also evidence of their practical significance. Though the rules for determining what is and what is not a good proof of correctness are clear, no comparable rules are usually enforced for determining the soundness of the data that is used to support the claim for practical significance. We consider here how we can flag the more common types of omission. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


title: Decomposing the Proof of Correctness of pipelined Microprocessors

authors:
Ravi Hosabettu
Mandayam K. Srivas
Ganesh Gopalakrishnan


title: Computing Reachable Control States of Systems Modeled with Uninterpreted Functions and Infinite Memory

authors:
Adrian J. Isles
Ramin Hojati
Robert K. Brayton


title: Design Constraints in Symbolic Model Checking

authors:
Matt Kaufmann
Andrew Martin
Carl Pixley


title: Structural Symmetry and Model Checking

authors:
Gurmeet Singh Manku
Ramin Hojati
Robert K. Brayton


title: Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking


title: Finite-State Analysis of Security Protocols


title: An ACL2 Proof of Write Invalidate Cache Coherence


title: The 'Test Model-Checking' Approach to the Verification of Formal Memory Models of Multiprocessors

authors:
Ratan Nalumasu
Rajnish Ghughal
Abdelillah Mokkedem
Ganesh Gopalakrishnan


title: Ten Years of Partial Order Reduction


title: A Toolset for Message Sequence Charts


title: Processor Verification with Precise Exeptions and Speculative Execution

authors:
Jun Sawada
Warren A. Hunt Jr.


title: A Comparison of Presburger Engines for EFSM Reachability

authors:
Thomas R. Shiple
James H. Kukula
Rajeev K. Ranjan


title: Formal Verification of Out-of-Order Execution Using Incremental Flushing

authors:
Jens U. Skakkebæk
Robert B. Jones
David L. Dill


title: Using Magnatic Disk Instead of Main Memory in the Murphi Verifier

authors:
Ulrich Stern
David L. Dill


title: Efficient Symbolic Detection of Global Properties in Distributed Systems

authors:
Scott D. Stoller
Yanhong A. Liu


title: On the Limitations of Ordered Representations of Functions


title: Model Checking LTL Using Net Unforldings


title: A Machine-Checked Proof of the Optimality of a Real-Time Scheduling Policy


title: Verifying Systems with Infinite but Regular State Spaces

authors:
Pierre Wolper
Bernard Boigelot


title: Model Checking for a First-Order Temporal Logic Using Multiway Decision Graphs

authors:
Ying Xu
Eduard Cerny
Xiaoyu Song
Francisco Corella
Otmane Aït Mohamed


title: Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis

authors:
Parosh Aziz Abdulla
Aurore Annichini
Saddek Bensalem
Ahmed Bouajjani
Peter Habermehl
Yassine Lakhnech


title: Handling Global Conditions in Parameterized System Verification

authors:
Parosh Aziz Abdulla
Ahmed Bouajjani
Bengt Jonsson
Marcus Nilsson


title: Timed Automata


title: Java Bytecode Verification by Model Checking

authors:
David A. Basin
Stefan Friedrich
Joachim Posegga
Harald Vogt


title: Model Checking the IBM Gigahertz Processor: An Abstraction Algorithm for High-Performance Netlists

authors:
Jason Baumgartner
Tamir Heyman
Vigyan Singhal
Adnan Aziz


title: Efficient Timed Reachability Analysis Using Clock Difference Diagrams

authors:
Gerd Behrmann
Kim Guldstrand Larsen
Justin Pearson
Carsten Weise
Wang Yi


title: Automated Verification of a Parametric Real-Time Program: The ABR Conformance Protocol

authors:
Béatrice Bérard
Laurent Fribourg


title: Verifiying Safety Properties of a Power PC Microprocessor Using Symbolic Model Checking without BDDs

authors:
Armin Biere
Edmund M. Clarke
Richard Raimi
Yunshan Zhu


title: Automatic Verification of Combinatorial and Pipelined FFT


title: Efficient Decision Procedures for Model Checking of Linear Time Logic Properties

authors:
Roderick Bloem
Kavita Ravi
Fabio Somenzi


title: Model Checking Based on Sequential ATPG

authors:
Vamsi Boppana
Sreeranga P. Rajan
Koichiro Takayama
Masahiro Fujita


title: On the Representation of Probabilities over Structured Domains

authors:
Marius Bozga
Oded Maler


title: Formal Methods for Conformance Testing: Theory Can Be Practical


title: Model Checking Partial State Spaces with 3-Valued Temporal Logics

authors:
Glenn Bruns
Patrice Godefroid


title: Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions

authors:
Randal E. Bryant
Steven M. German
Miroslav N. Velev


title: A Toolbox for the Analysis of Discrete Event Dynamic Systems

authors:
Peter Buchholz
Peter Kemper


title: Latency Insensitive Protocols

authors:
Luca P. Carloni
Kenneth L. McMillan
Alberto L. Sangiovanni-Vincentelli


title: The Mathematical Foundation fo Symbolic Trajectory Evaluation


title: NUSMV: A New Symbolic Model Verifier

authors:
Alessandro Cimatti
Edmund M. Clarke
Fausto Giunchiglia
Marco Roveri


title: Improved Automata Generation for Linear Temporal Logic

authors:
Marco Daniele
Fausto Giunchiglia
Moshe Y. Vardi


title: Experience with Predicate Abstraction

authors:
Satyaki Das
David L. Dill
Seungjoon Park


title: Alternative Approaches to Hardware Verification (abstract)


title: Stutter-Invariant Languages, omega-Automata, and Temporal Logic


title: Mechanizing Proofs of Computation Equivalence

authors:
Marcelo Glusman
Shmuel Katz


title: Assume-Guarantee Refinement Between Different Time Scales

authors:
Thomas A. Henzinger
Shaz Qadeer
Sriram K. Rajamani


title: Verifying Sequential Consistency on Shared-Memory Multiprocessor Systems


title: TIPPtool: Compositional Specification and Analysis of Markovian Performance Models

authors:
Holger Hermanns
Vassilis Mertsiotakis
Markus Siegle


title: Test Generation Derived from Model-Checking

authors:
Thierry Jéron
Pierre Morel


title: A Theory of Restrictions for Logics and Automata


title: Model Checking of Safety Properties

authors:
Orna Kupferman
Moshe Y. Vardi


title: A Complete Finite Prefix for Process Algebra

authors:
Rom Langerak
Ed Brinksma


title: Stepwise CTL Model Checking of State/Event Systems

authors:
Jørn Lind-Nielsen
Henrik Reif Andersen


title: Verification of Parameterized Systems by Dynamic Induction on Diagrams

authors:
Zohar Manna
Henny Sipma


title: Linking Theorem Proving and Model-Checking with Well-Founded Bisimulation

authors:
Panagiotis Manolios
Kedar S. Namjoshi
Robert Summers


title: Elementary Microarchitecture Algebra

authors:
John Matthews
John Launchbury


title: Efficient Analysis of Cyclic Definitions

authors:
Kedar S. Namjoshi
Robert P. Kurshan


title: Deciding Equality Formulas by Small Domains Instantiations

authors:
Amir Pnueli
Yoav Rodeh
Ofer Strichman
Michael Siegel


title: Validation of Pipelined Processor Designs Using Esterel Tools: A Case Study

authors:
S. Ramesh
Purandar Bhaduri


title: Abstract and Model Check While You Prove

authors:
Hassen Saïdi
Natarajan Shankar


title: PIL/SETHEO: A Tool for the Automatic Analysis of Authentication Protocols


title: The Compositional Specification of Timed Systems - A Tutorial


title: Automatic Verification of Abstract State Machines


title: Optimizing Symbolic Model Checking for Constraint-Rich Models

authors:
Bwolen Yang
Reid G. Simmons
Randal E. Bryant
David R. O'Hallaron

abstract: This paper presents optimizations for verifying systems with complex time-invariant constraints. These constraints arise naturally from modeling physical systems, e.g., in establishing the relationship between different components in a system. To verify constraint-rich systems, we propose two new optimizations. The first optimization is a simple, yet powerful, extension of the conjunctivepartitioning algorithm. The second is a collection of BDD-based macro-extraction and macro-expansion algorithms to remove state variables. We showthat these two optimizations are essential in verifying constraint-rich problems; in particular, this work has enabled the verification of fault diagnosis models of the Nomad robot (an Antarctic meteorite explorer) and of the NASA Deep Space One spacecraft.


title: FoCs: Automatic Generation of Simulation Checkers from Formal Specifications

authors:
Yael Abarbanel
Ilan Beer
Leonid Gluhovsky
Sharon Keidar
Yaron Wolfsthal


title: Unfoldings of Unbounded Petri Nets

authors:
Parosh Aziz Abdulla
S. Purushothaman Iyer
Aletta Nylén


title: Invited Tutorial: Verification of Infinite-State and Parameterized Systems

authors:
Parosh Aziz Abdulla
Bengt Jonsson


title: Detecting Errors Before Reaching Them

authors:
Luca de Alfaro
Thomas A. Henzinger
Freddy Y. C. Mang


title: Efficient Reachability Analysis of Hierarchical Reactive Machines

authors:
Rajeev Alur
Radu Grosu
Michael McDougall


title: Symbolic Techniques for Parametric Reasoning about Counter and Clock Systems

authors:
Aurore Annichini
Eugene Asarin
Ahmed Bouajjani


title: Bounded Model Construction for Monadic Second-Order Logics

authors:
Abdelwaheb Ayari
David A. Basin


title: Decision Procedures for Inductive Boolean Functions Based on Alternating Automata

authors:
Abdelwaheb Ayari
David A. Basin
Felix Klaedtke


title: Model Checking Continuous-Time Markov Chains by Transient Analysis

authors:
Christel Baier
Boudewijn R. Haverkort
Holger Hermanns
Joost-Pieter Katoen


title: An Abstraction Algorithm for the Verification of Generalized C-Slow Designs

authors:
Jason Baumgartner
Anson Tripp
Adnan Aziz
Vigyan Singhal
Flemming Andersen


title: Distributing Timed Model Checking - How the Search Order Matters

authors:
Gerd Behrmann
Thomas Hune
Frits W. Vaandrager


title: The STATEMATE Verification Environment - Making It Real

authors:
Tom Bienmüller
Werner Damm
Hartmut Wittke


title: Regular Model Checking

authors:
Ahmed Bouajjani
Bengt Jonsson
Marcus Nilsson
Tayssir Touili


title: Are Timed Automata Updatable?

authors:
Patricia Bouyer
Catherine Dufourd
Emmanuel Fleury
Antoine Petit


title: IF: A Validation Environment for Timed Asynchronous Systems

authors:
Marius Bozga
Jean-Claude Fernandez
Lucian Ghirvu
Susanne Graf
Jean-Pierre Krimm
Laurent Mounier


title: Boolean Satisfiability with Transitivity Constraints

authors:
Randal E. Bryant
Miroslav N. Velev


title: Model-Checking for Hybrid Systems by Quotienting and Constraints Solving

authors:
Franck Cassez
François Laroussinie


title: Temporal-Locig Queries


title: Counterexample-Guided Abstraction Refinement

authors:
Edmund M. Clarke
Orna Grumberg
Somesh Jha
Yuan Lu
Helmut Veith


title: TAPS: A First-Order Verifier for Cryptographic Protocols


title: A Proof-Carrying Code Architecture for Java

authors:
Christopher Colby
Peter Lee
George C. Necula


title: Binary Reachability Analysis of Discrete Pushdown Timed Automata

authors:
Zhe Dang
Oscar H. Ibarra
Tevfik Bultan
Richard A. Kemmerer
Jianwen Su


title: Automatic Verification of Parameterized Cache Coherence Protocols


title: Efficient Algorithms for Model Checking Pushdown Systems

authors:
Javier Esparza
David Hansel
Peter Rossmanith
Stefan Schwoon


title: Prioritized Traversal: Efficient Reachability Analysis for Verification and Falsification

authors:
Ranan Fraer
Gila Kamhi
Barukh Ziv
Moshe Y. Vardi
Limor Fix


title: PET: An Interactive Software Testing Tool

authors:
Elsa L. Gunter
Robert P. Kurshan
Doron A. Peled


title: Achieving Scalability in Parallel Reachability Analysis of Very Large Circuits

authors:
Tamir Heyman
Daniel Geist
Orna Grumberg
Assaf Schuster


title: Verifying Advanced Microarchitectures that Support Speculation and Exceptions

authors:
Ravi Hosabettu
Ganesh Gopalakrishnan
Mandayam K. Srivas


title: Building Circuits from Relations

authors:
James H. Kukula
Thomas R. Shiple


title: An Automata-Theoretic Approach to Reasoning about Infinite-State Systems

authors:
Orna Kupferman
Moshe Y. Vardi


title: Invited Tutorial: Boolean Satisfiability Algorithms and Applications in Electronic Design Automation

authors:
João Marques-Silva
Karem A. Sakallah


title: Induction in Compositional Model Checking

authors:
Kenneth L. McMillan
Shaz Qadeer
James B. Saxe


title: Invited Address: Applying Formal Methods to Cryptographic Protocol Analysis


title: Syntactic Program Transformations for Automatic Abstraction

authors:
Kedar S. Namjoshi
Robert P. Kurshan


title: On the Competeness of Compositional Reasoning

authors:
Kedar S. Namjoshi
Richard J. Trefler


title: Integrating WS1S with PVS

authors:
Sam Owre
Harald Rueß


title: Keynote Address: Abstraction, Composition, Symmetry, and a Little Deduction: The Remedies to State Explosion


title: Liveness and Acceleration in Parameterized Verification

authors:
Amir Pnueli
Elad Shahar


title: XMC: A Logic-Programming-Based Verification Toolset

authors:
C. R. Ramakrishnan
I. V. Ramakrishnan
Scott A. Smolka
Yifei Dong
Xiaoqun Du
Abhik Roychoudhury
V. N. Venkatakrishnan


title: Verification Diagrams Revisited: Disjunctive Invariants for Easy Verification


title: Mechanical Verification of an Ideal Incremental ABR Conformance

authors:
Michaël Rusinowitch
Sorin Stratulat
Francis Klay


title: Tuning SAT Checkers for Bounded Model Checking


title: Efficient Büchi Automata from LTL Formulae

authors:
Fabio Somenzi
Roderick Bloem


title: Efficient Detection of Global Properties in Distributed Systems Using Partial-Order Methods

authors:
Scott D. Stoller
Leena Unnikrishnan
Yanhong A. Liu


title: Formal Verification of VLIW Microprocessors with Speculative Execution


title: A Discrete Strategy Improvement Algorithm for Solving Parity Games

authors:
Jens Vöge
Marcin Jurdzinski


title: Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking

authors:
Poul Frederick Williams
Armin Biere
Edmund M. Clarke
Anubhav Gupta

abstract: In this paper we show how to do symbolic model checking using Boolean Expression Diagrams (BEDs), a non-canonical representation for Boolean formulas, instead of Binary Decision Diagrams (BDDs), the traditionally used canonical representation. The method is based on standard fixed point algorithms, combined with BDDs and SAT-solvers to perform satisfiability checking. As a result we are able to model check systems for which standard BDD-based methods fail. For example, we model check a liveness property of a 256 bit shift-and-add multiplier and we are able to find a previously undetected bug in the specification of a 16 bit multiplier. As opposed to Bounded Model Checking (BMC) our method is complete in practice.


title: VINAS-P: A Tool for Trace Theoretic Verification of Timed Asynchronous Circuits


title: Job-Shop Scheduling Using Timed Automata

authors:
Yasmina Abdeddaïm
Oded Maler


title: Model Checking the World Wide Web


title: Analysis of Recursive State Machines

authors:
Rajeev Alur
Kousha Etessami
Mihalis Yannakakis


title: Verifying Network Protocol Implementations by Symbolic Refinement Checking

authors:
Rajeev Alur
Bow-Yaw Wang


title: Rtdt: A Front-End for Efficient Model Checking of Synchronous Timing Diagrams

authors:
Nina Amla
E. Allen Emerson
Robert P. Kurshan
Kedar S. Namjoshi


title: TReX: A Tool for Reachability Analysis of Complex Systems

authors:
Aurore Annichini
Ahmed Bouajjani
Mihaela Sighireanu


title: Using Timestamping and History Variables to Verify Sequential Consistency


title: Parameterized Verification with Automatically Computed Inductive Assertions

authors:
Tamarah Arons
Amir Pnueli
Sitvanit Ruah
Jiazhao Xu
Lenore D. Zuck


title: Model Checking with Formula-Dependent Abstract Models

authors:
Alexander Asteroth
Christel Baier
Ulrich Aßmann


title: The SLAM Toolkit

authors:
Thomas Ball
Sriram K. Rajamani


title: The Temporal Logic Sugar

authors:
Ilan Beer
Shoham Ben-David
Cindy Eisner
Dana Fisman
Anna Gringauze
Yoav Rodeh


title: Formalizing a JVML Verifier for Initialization in a Theorem Prover


title: Efficient Model Checking Via Büchi Tableau Automata

authors:
Girish Bhat
Rance Cleaveland
Alex Groce


title: Finding Bugs in an Alpha Microprocessor Using Satisfiability Solvers

authors:
Per Bjesse
Tim Leonard
Abdel Mokkedem


title: µCRL: A Toolset for Analysing Algebraic Specifications

authors:
Stefan Blom
Wan J. Fokkink
Jan Friso Groote
Izak van Langevelde
Bert Lisser
Jaco van de Pol


title: Meta-BDDs: A Decomposed Representation for Layered Symbolic Manipulation of Boolean Functions


title: A Practical Approach to Coverage in Model Checking

authors:
Hana Chockler
Orna Kupferman
Robert P. Kurshan
Moshe Y. Vardi


title: TAXYS: A Tool for the Development and Verification of Real-Time Embedded Systems

authors:
Etienne Closse
Michel Poize
Jacques Pulou
Joseph Sifakis
Patrick Venier
Daniel Weil
Sergio Yovine


title: Benefits of Bounded Model Checking at an Industrial Setting

authors:
Fady Copty
Limor Fix
Ranan Fraer
Enrico Giunchiglia
Gila Kamhi
Armando Tacchella
Moshe Y. Vardi


title: Iterating Transducers

authors:
Dennis Dams
Yassine Lakhnech
Martin Steffen


title: Binary Reachability Analysis of Pushdown Timed Automata with Dense Clocks


title: Attacking Symbolic State Explosion

authors:
Giorgio Delzanno
Jean-François Raskin
Laurent Van Begin


title: A Fast Bisimulation Algorithm

authors:
Agostino Dovier
Carla Piazza
Alberto Policriti


title: A BDD-Based Model Checker for Recursive Programs

authors:
Javier Esparza
Stefan Schwoon


title: ICS: Integrated Canonizer and Solver

authors:
Jean-Christophe Filliâtre
Sam Owre
Harald Rueß
Natarajan Shankar


title: Fast LTL to Büchi Automata Translation

authors:
Paul Gastin
Denis Oddoux


title: Distributed Symbolic Model Checking for µ-Calculus

authors:
Orna Grumberg
Tamir Heyman
Assaf Schuster


title: Microarchitecture Verification by Compositional Model Checking

authors:
Ranjit Jhala
Kenneth L. McMillan


title: BooStER: Speeding Up RTL Property Checking of Digital Designs by Word-Level Abstarction


title: Transformation-Based Verification Using Generalized Retiming

authors:
Andreas Kuehlmann
Jason Baumgartner


title: Automated Verification of a Randomized Distributed Consensus Protocol Using Cadence SMV and PRISM

authors:
Marta Z. Kwiatkowska
Gethin Norman
Roberto Segala


title: As Cheap as Possible: Efficient Cost-Optimal Reachability for Priced Timed Automata

authors:
Kim Guldstrand Larsen
Gerd Behrmann
Ed Brinksma
Ansgar Fehnker
Thomas Hune
Paul Pettersson
Judi Romijn


title: Java Bytecode Verification: An Overview


title: Truth/SLC - A Parallel Verification Platform for Concurrent Systems

authors:
Martin Leucker
Thomas Noll


title: SDLcheck: A Model Checking Tool

authors:
Vladimir Levin
Hüsnü Yenigün


title: A Unifying Model Checking Approach for Safety Properties of Parameterized Systems


title: CLEVER: Divide and Conquer Combinational Logic Equivalence VERification with False Negative Elimination

authors:
John Moondanos
Carl-Johan H. Seger
Ziyad Hanna
Daher Kaiss


title: Rewriting for Symbolic Execution of State Machine Models


title: Towards Efficient Verification of Arithmetic Algorithms over Galois Fields GF(2m)

authors:
Sumio Morioka
Yasunao Katayama
Toshiyuki Yamane


title: Certifying Model Checkers


title: Software Documentation and the Verification Process


title: Finite Instantiations in Equivalence Logic with Uninterpreted Functions

authors:
Yoav Rodeh
Ofer Strichman


title: Automated Inductive Verification of Parameterized Protocols

authors:
Abhik Roychoudhury
I. V. Ramakrishnan


title: EASN: Integrating ASN.1 and Model Checking

authors:
Vivek K. Shanbhag
K. Gopinath
Markku Turunen
Ari Ahtiainen
Matti Luukkainen


title: Symmetry and Reduced Symmetry in Model Checking

authors:
A. Prasad Sistla
Patrice Godefroid


title: AGVI - Automatic Generation, Verification, and Implementation of Security Protocols

authors:
Dawn Xiaodong Song
Adrian Perrig
Doantam Phan


title: EVC: A Validity Checker for the Logic of Equality with Uninterpreted Functions and Memories, Exploiting Positive Equality, and Conservative Transformations

authors:
Miroslav N. Velev
Randal E. Bryant


title: Automatic Abstraction for Verification of Timed Circuits and Systems

authors:
Hao Zheng
Eric Mercer
Chris J. Myers


title: Regular Tree Model Checking

authors:
Parosh Aziz Abdulla
Bengt Jonsson
Pritha Mahata
Julien d'Orso


title: Exploiting Behavioral Hierarchy for Efficient Model Checking

authors:
Rajeev Alur
Michael McDougall
Zijiang Yang


title: The AVISS Security Protocol Analysis Tool

authors:
Alessandro Armando
David A. Basin
Mehdi Bouallagui
Yannick Chevalier
Luca Compagna
Sebastian Mödersheim
Michaël Rusinowitch
Mathieu Turuani
Luca Viganò
Laurent Vigneron


title: The d/dt Tool for Verification of Hybrid Systems

authors:
Eugene Asarin
Thao Dang
Oded Maler


title: SPeeDI - A Verification Tool for Polygonal Hybrid Systems

authors:
Eugene Asarin
Gordon J. Pace
Gerardo Schneider
Sergio Yovine


title: Combining Symmetry Reduction and Under-Approximation for Symbolic Model Checking

authors:
Sharon Barner
Orna Grumberg


title: Symbolic Localization Reduction with Reconstruction Layering and Backtracking

authors:
Sharon Barner
Daniel Geist
Anna Gringauze


title: Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT

authors:
Clark W. Barrett
David L. Dill
Aaron Stump


title: Property Checking via Structural Analysis

authors:
Jason Baumgartner
Andreas Kuehlmann
Jacob A. Abraham


title: PathFinder: A Tool for Design Exploration

authors:
Shoham Ben-David
Anna Gringauze
Baruch Sterin
Yaron Wolfsthal


title: Semi-formal Bounded Model Checking

authors:
Jesse D. Bingham
Alan J. Hu


title: State Space Reduction by Proving Confluence

authors:
Stefan Blom
Jaco van de Pol


title: Extrapolating Tree Transformations

authors:
Ahmed Bouajjani
Tayssir Touili


title: IF-2.0: A Validation Environment for Component-Based Real-Time Systems

authors:
Marius Bozga
Susanne Graf
Laurent Mounier


title: Algorithmic Verification of Invalidation-Based Protocols

authors:
Marco Bozzano
Giorgio Delzanno


title: Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions

authors:
Randal E. Bryant
Shuvendu K. Lahiri
Sanjit A. Seshia


title: Mixing Forward and Backward Traversals in Guided-Prioritized BDD-Based Verification

authors:
Gianpiero Cabodi
Sergio Nocco
Stefano Quer


title: Interface Compatibility Checking for Software Modules

authors:
Arindam Chakrabarti
Luca de Alfaro
Thomas A. Henzinger
Marcin Jurdzinski
Freddy Y. C. Mang


title: Synchronous and Bidirectional Component Interfaces

authors:
Arindam Chakrabarti
Luca de Alfaro
Thomas A. Henzinger
Freddy Y. C. Mang


title: Shared Memory Consistency Protocol Verification Against Weak Memory Models: Refinement via Model-Checking

authors:
Prosenjit Chatterjee
Hemanthkumar Sivaraj
Ganesh Gopalakrishnan


title: chi-Chek: A Multi-valued Model-Checker

authors:
Marsha Chechik
Arie Gurfinkel
Benet Devereux


title: Automated Unbounded Verification of Security Protocols

authors:
Yannick Chevalier
Laurent Vigneron


title: NuSMV 2: An OpenSource Tool for Symbolic Model Checking

authors:
Alessandro Cimatti
Edmund M. Clarke
Enrico Giunchiglia
Fausto Giunchiglia
Marco Pistore
Marco Roveri
Roberto Sebastiani
Armando Tacchella


title: SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques

authors:
Edmund M. Clarke
Anubhav Gupta
James H. Kukula
Ofer Strichman

abstract: We describe new techniques for model checking in the counterexample guided abstraction/refinement framework. The abstraction phase ‘hides’ the logic of various variables, hence considering them as inputs. This type of abstraction may lead to ‘spurious’ counterexamples, i.e. traces that can not be simulated on the original (concrete) machine. We check whether a counterexample is real or spurious with a SAT checker. We then use a combination of Integer Linear Programming (ILP) and machine learning techniques for refining the abstraction based on the counterexample. The process is repeated until either a real counterexample is found or the property is verified. We have implemented these techniques on top of the model checker NuSMV and the SAT solver Chaff. Experimental results prove the viability of these new techniques. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


title: Practical Methods for Proving Program Termination

authors:
Michael Colón
Henny Sipma


title: On Abstraction in Software Verification

authors:
Patrick Cousot
Radhia Cousot


title: Abstracting C with abC

authors:
Dennis Dams
William Hesse
Gerard J. Holzmann


title: A Modular Checker for Multithreaded Programs

authors:
Cormac Flanagan
Shaz Qadeer
Sanjit A. Seshia


title: Automatic Abstraction Using Generalized Model Checking

authors:
Patrice Godefroid
Radha Jagadeesan


title: AMC: An Adaptive Model Checker

authors:
Alex Groce
Doron A. Peled
Mihalis Yannakakis


title: Fair Simulation Minimization

authors:
Sankar Gurumurthy
Roderick Bloem
Fabio Somenzi


title: On Discrete Modeling and Model Checking for Nonlinear Analog Systems

authors:
Walter Hartong
Lars Hedrich
Erich Barke


title: The Symbolic Approach to Hybrid Systems


title: Temporal-Safety Proofs for Systems Code

authors:
Thomas A. Henzinger
Ranjit Jhala
Rupak Majumdar
George C. Necula
Grégoire Sutre
Westley Weimer


title: Software Analysis and Model Checking


title: Formal Verification of Complex Out-of-Order Pipelines by Combining Model-Checking and Theorem-Proving


title: Canonical Prefixes of Petri Net Unfoldings

authors:
Victor Khomenko
Maciej Koutny
Walter Vogler


title: Model Checking Linear Properties of Prefix-Recognizable Systems

authors:
Orna Kupferman
Nir Piterman
Moshe Y. Vardi


title: Compressing Transitions for Model Checking

authors:
Robert P. Kurshan
Vladimir Levin
Hüsnü Yenigün


title: Applying SAT Methods in Unbounded Symbolic Model Checking


title: Liveness with (0, 1, infty)-Counter Abstraction

authors:
Amir Pnueli
Jessie Xu
Lenore D. Zuck


title: Vacuum Cleaning CTL Formulae

authors:
Mitra Purandare
Fabio Somenzi


title: Conformance Checking for Models of Asynchronous Message Passing Software

authors:
Sriram K. Rajamani
Jakob Rehof


title: Using Canonical Representations of Solutions to Speed Up Infinite-State Model Checking

authors:
Tatiana Rybina
Andrei Voronkov


title: Deciding Separation Formulas with SAT

authors:
Ofer Strichman
Sanjit A. Seshia
Randal E. Bryant