By series

A conference on automated verification with an Asian base, covering model checking, synthesis, automata-theoretic methods and the analysis of hybrid and probabilistic systems. Each edition has its own site rather than a permanent one.

The main conference series on automated deduction, running since 1974: theorem provers, proof search, unification, decision procedures and the systems that implement them. It alternates with IJCAR, and its steering body also runs the CADE ATP System Competition.

The main annual conference on computer-aided verification, running since 1989. CAV covers the theory and practice of automatically proving things about hardware and software — model checking, SAT and SMT, abstract interpretation, synthesis and the tools built on them — and is one of the two or three venues where the field's results first appear.

The annual conference of the European Association for Computer Science Logic, on logic as it is used in computer science — proof theory, model theory, finite model theory and their applications to verification and databases.

One of the ETAPS conferences. ESOP is about programming languages and systems from the design side: type systems, semantics, program logics and the analyses that follow from them, where TACAS beside it takes the tools.

The symposium of Formal Methods Europe, held every year or two since 1987 and the broadest gathering in the field: specification, refinement, proof, and reports of what happened when these were used on real systems.

A conference on formal methods for open, object-based distributed systems, run from 1996. It merged with FORTE in 2007, so citations to it stop there and continue under the joint name.

The theory conference within ETAPS: semantics, automata, type theory, categorical models and the mathematics underlying programming and verification.

India's main theoretical computer science conference, held every December since 1981 and run by IARCS with ACM India. It takes foundational work across the field — algorithms, complexity, logic, semantics, verification — and has published through LIPIcs since 2008, so recent volumes are open access.

A conference on combining formal methods rather than choosing between them — pairing state-based specification with process algebra, proof with model checking, and so on. Each edition has its own site.

A symposium on putting formal methods to work, organised around themed tracks rather than a general call. Sessions pair short talks with long panel discussions, deliberately mixing academics with people who have to adopt these tools in industry, and the proceedings run to several volumes a year.

A small biennial conference on deriving programs from specifications: calculational methods, algebra of programming, and the mathematics of getting from a problem statement to code that provably solves it.

NASA's formal methods symposium, on techniques with a path into safety-critical practice — aerospace software, autonomy, and the verification of systems whose failure is not recoverable.

The Passive and Active Measurement conference: empirical work on how the internet actually behaves — routing, latency, censorship, traffic — measured rather than modelled. Each edition has its own site; proceedings appear in Springer's LNCS.

A conference on where software engineering and formal methods meet: applying rigorous techniques at the scale and under the constraints of actual software development.

One of the ETAPS conferences, held every spring. TACAS is where verification tools are presented rather than only techniques: model checkers, SMT-based analysers, static analysers and the algorithms behind them, with a long-standing emphasis on artefacts that others can run. It also hosts the annual SV-COMP competition on software verification.

A European conference series on the theory and practice of software development, running from 1985 to 1997. It was folded into ETAPS, so its later editions are cited as ETAPS conferences and TAPSOFT itself is closed.

A conference on theorem proving in higher-order logics, run from 1988 until 2009. It became ITP, the Interactive Theorem Proving conference, which is where its community publishes now.

A conference on verified software, founded around the grand-challenge idea of a verifying compiler: proof-carrying tools, verified components, and experiments in building software that comes with its guarantees.

The annual conference of the European Association for Computer Science Logic, on logic as it is used in computer science — proof theory, model theory, finite model theory and their applications to verification and databases.