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]. A newer bridge even re-expresses hardware as a C program, reusing mature software analysers. Because each domain grows its techniques around its own bottlenecks, comparing them fairly, 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