Topics of Interest


Topics of interest include

  • Standardization of expressive languages. Formats to represent systems, formulas, proofs, counterexamples. Translation between specification languages. Benchmarks and competitions for auto- mated reasoning, verification, analysis, synthesis.
  • Decision procedures: Decision procedures for new classes of constraints. SAT and SMT implementation and certification. Encoding synthesis and analysis problems into SMT. Description logics and scalable reasoning about knowledge bases.
  • Transition system analysis: Abstraction-based approaches and refinement for verification of infinite-state systems. Constraint-based program analysis. Data-flow analysis for complex domains. Extracting transition systems from programming languages and bytecodes.
  • High-level synthesis: New algorithms for synthesis from high-level specifications. Extending decision procedures to perform synthesis tasks. Connections between invariant generation and code synthesis.


The scope of VERIFY includes topics such as

  • ATP techniques in verification
  • Case studies (specification and verification)
  • Combination of verification tools
  • Compositional and modular reasoning
  • Experience reports on using formal methods
  • Formal methods for fault tolerance
  • Gaps between problems and techniques
  • Information-flow control
  • Integration of ATPs and CASE-tools
  • Management of change
  • Refinement and decomposition
  • Reliability of mobile computing
  • Reuse of specifications and proofs
  • Safety-critical systems
  • Security models
  • Tool support for formal methods