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