Formalisation writes a system's meaning in precise mathematics, so that claims about it can be proved rather than argued. Proof assistants, such as Coq (recently renamed Rocq) and Isabelle, take this furthest, letting a person write the proof while the machine checks every step, which gives very high trust [1]. For a programming language, the thing being formalised is its semantics, a precise account of how its programs execute [2]. With a semantics in place, one can define when two programs are equivalent, often through bisimulation, and then prove that a refactoring or an optimising compiler preserves behaviour [3].
Automata theory studies simple machines that recognise patterns. A finite automaton reads a string over a fixed, finite alphabet and either accepts or rejects it, and the languages it can recognise are the regular ones [4]. Many systems, though, handle data values from an unbounded domain, so register automata extend the model to an infinite alphabet by storing values in a few registers for later comparison [5]. This extra power has a cost: some questions that are easy for finite automata become hard, or even undecidable. A key example is the universality problem, which asks whether an automaton accepts every possible word, and which is closely tied to complementing its language [6]. For these richer automata universality is undecidable in general, yet it can become decidable once the model is suitably restricted.
Model checkers are automatic tools that explore a system's reachable states. Concurrent software is difficult for them, because its threads can interleave in enormous numbers of orders, a classic source of state-space explosion. Partial order reduction (POR) tackles this by exploring only one representative of each set of equivalent interleavings, using the fact that independent actions commute [7]. Abstraction addresses the same explosion from another side, by dropping detail while keeping enough to decide the property, and making abstraction and POR cooperate soundly is a real challenge [8]. Hardware verification faces its own pressures, and a common route is to translate a design into a standard format and hand it to a backend solver [9]. Because each domain grows its techniques around its own bottlenecks, comparing them, or carrying an algorithm from one domain to another, is rarely straightforward.
Keywords to look up: formalisation · formal semantics · proof assistant (Coq/Rocq) · machine-checked proof · program equivalence · bisimulation · verified compiler · finite automaton · regular language · infinite alphabet / register automaton · universality · complementation · decidability · concurrency · interleaving · state-space explosion · partial order reduction (POR) · abstraction · hardware model checking · encoding / exchange format.
Sources
- Y. Bertot, P. Castéran. Interactive Theorem Proving and Program Development (Coq'Art). Springer, 2004. doi.org/10.1007/978-3-662-07964-5
- G. Winskel. The Formal Semantics of Programming Languages. MIT Press, 1993. ISBN 978-0-262-23169-5.
- D. Sangiorgi. Introduction to Bisimulation and Coinduction. Cambridge University Press, 2011. doi.org/10.1017/CBO9780511777110
- J. E. Hopcroft, R. Motwani, J. D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, 3rd ed., 2006. ISBN 978-0-321-45536-9.
- M. Kaminski, N. Francez. "Finite-Memory Automata." Theoretical Computer Science, 1994. doi.org/10.1016/0304-3975(94)90242-9
- L. Segoufin. "Automata and Logics for Words and Trees over an Infinite Alphabet." CSL, 2006. doi.org/10.1007/11874683_3
- D. Peled. "All from One, One for All: On Model Checking Using Representatives." CAV, 1993. doi.org/10.1007/3-540-56922-7_34
- E. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith. "Counterexample-Guided Abstraction Refinement for Symbolic Model Checking." JACM, 2003. doi.org/10.1145/876638.876643
- A. Biere, A. Cimatti, E. Clarke, Y. Zhu. "Symbolic Model Checking without BDDs." TACAS, 1999. doi.org/10.1007/3-540-49059-0_14