Jump to content

Formal methods

From Wikipedia, the free encyclopedia
(Redirected from Formal Methods)

In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems.[1] The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.[2]

Formal methods employ a variety of theoretical computer science fundamentals, including logic calculi, formal languages, automata theory, control theory, program semantics, type systems, and type theory.[3]

History

[edit]

Reasoning mathematically about programs predates the discipline's name. Alan Turing sketched a correctness argument for a routine in 1949,[4] and in the late 1960s Robert W. Floyd and Tony Hoare established the axiomatic tradition of program proof that became Hoare logic.[5][6] Edsger W. Dijkstra's weakest-precondition calculus gave a systematic way to derive programs from specifications,[7] and model-oriented specification languages such as VDM and the Z notation were developed during the 1970s.

A second tradition grew out of temporal logic. Amir Pnueli proposed it in 1977 as a language for specifying the behaviour of reactive programs,[8] and model checking was introduced independently by Edmund M. Clarke and E. Allen Emerson and by Jean-Pierre Queille and Joseph Sifakis in the early 1980s, work for which the three shared the 2007 Turing Award. Symbolic model checking with binary decision diagrams raised the size of systems that could be analysed by orders of magnitude,[9] and bounded model checking built on SAT solvers extended it further.[10]

Industrial interest was sharpened by costly defects such as the 1994 Pentium FDIV bug, which prompted processor vendors to invest heavily in hardware verification. From the 2000s onwards, maturing SMT solvers and proof assistants made it practical to verify complete systems rather than isolated components.[11]

Uses

[edit]

Formal methods can be applied at various points through the development process.

Specification

[edit]

Formal methods may be used to give a formal description of the system to be developed, at whatever level of detail desired. Further formal methods may depend on this specification to synthesize a program or to verify the correctness of a system.

Alternatively, specification may be the only stage in which formal methods are used. By writing a specification, ambiguities in the informal requirements can be discovered and resolved. Additionally, engineers can use a formal specification as a reference to guide their development processes.[12]

The need for formal specification systems has been noted for years. In the ALGOL 58 report,[13] John Backus presented a formal notation for describing programming language syntax, later named Backus normal form then renamed Backus–Naur form (BNF).[14] Backus also wrote that a formal description of the meaning of syntactically valid ALGOL programs was not completed in time for inclusion in the report, stating that it "will be included in a subsequent paper." However, no paper describing the formal semantics was ever released.[15]

Synthesis

[edit]

Program synthesis is the process of automatically creating a program that conforms to a specification. Deductive synthesis approaches rely on a complete formal specification of the program, whereas inductive approaches infer the specification from examples. Synthesizers perform a search over the space of possible programs to find a program consistent with the specification. Because of the size of this search space, developing efficient search algorithms is one of the major challenges in program synthesis.[16]

Verification

[edit]

Formal verification is the use of software tools to prove properties of a formal specification, or to prove that a formal model of a system implementation satisfies its specification.

Once a formal specification has been developed, the specification may be used as the basis for proving properties of the specification, and by inference, properties of the system implementation.

Sign-off verification

[edit]

Sign-off verification is the use of a formal verification tool that is highly trusted. Such a tool can replace traditional verification methods (the tool may even be certified).[17]

Human-directed proof

[edit]

Sometimes, the motivation for proving the correctness of a system is not the obvious need for reassurance of the correctness of the system, but a desire to understand the system better. Consequently, some proofs of correctness are produced in the style of mathematical proof: handwritten (or typeset) using natural language, using a level of informality common to such proofs. A "good" proof is one that is readable and understandable by other human readers.

Critics of such approaches point out that the ambiguity inherent in natural language allows errors to be undetected in such proofs; often, subtle errors can be present in the low-level details typically overlooked by such proofs. Additionally, the work involved in producing such a good proof requires a high level of mathematical sophistication and expertise.

Interactive theorem proving

[edit]

Proof assistants occupy a middle ground between wholly human-directed and wholly automated proof. The user directs the argument, typically by applying tactics, while the tool records each step and mechanically checks the resulting proof. Because the finished proof is checked by a comparatively small and stable kernel, the much larger body of search and automation surrounding it need not itself be trusted.[18] Systems in common use include Isabelle/HOL, the Rocq Prover (named Coq until 2025), Lean, Agda, HOL4, PVS and ACL2. Interactive proof underlies most of the largest verified software artifacts, including the seL4 microkernel and the CompCert compiler, and is increasingly combined with automated back ends so that routine obligations are discharged by solvers while difficult ones are proved by hand.

Automated proof

[edit]

In contrast, there is increasing interest in producing proofs of correctness of such systems by automated means. Automated techniques fall into four general categories:

  • Automated theorem proving, in which a system attempts to produce a formal proof from scratch, given a description of the system, a set of logical axioms, and a set of inference rules.
  • Model checking, in which a system verifies certain properties by means of an exhaustive search of all possible states that a system could enter during its execution.
  • Abstract interpretation, in which a system verifies an over-approximation of a behavioural property of the program, using a fixpoint computation over a (possibly complete) lattice representing it.
  • Deductive verification, in which a program annotated with preconditions, postconditions and loop invariants is translated, in the tradition of Hoare logic, into logical verification conditions whose validity is then discharged automatically by an SMT solver or interactively in a proof assistant.[19]

Some automated theorem provers require guidance as to which properties are "interesting" enough to pursue, while others work without human intervention. Model checkers can quickly get bogged down in checking millions of uninteresting states if not given a sufficiently abstract model.

Proponents of such systems argue that the results have greater mathematical certainty than human-produced proofs, since all the tedious details have been algorithmically verified. The training required to use such systems is also less than that required to produce good mathematical proofs by hand, making the techniques accessible to a wider variety of practitioners.

Critics note that some of those systems are like oracles: they make a pronouncement of truth, yet give no explanation of that truth. There is also the problem of "verifying the verifier"; if the program that aids in the verification is itself unproven, there may be reason to doubt the soundness of the produced results. Some modern model checking tools produce a "proof log" detailing each step in their proof, making it possible to perform, given suitable tools, independent verification.

The main feature of the abstract interpretation approach is that it provides a sound analysis, i.e. no false negatives are returned. Moreover, it is efficiently scalable, by tuning the abstract domain representing the property to be analyzed, and by applying widening operators[20] to get fast convergence.

Techniques

[edit]

Formal methods includes a number of different techniques.

Specification languages

[edit]

The design of a computing system can be expressed using a specification language, which is a formal language that includes a proof system. Using this proof system, formal verification tools can reason about the specification and establish that a system adheres to the specification.[21]

Binary decision diagrams

[edit]

A binary decision diagram is a data structure that represents a Boolean function.[22] If a Boolean formula expresses that an execution of a program conforms to the specification, a binary decision diagram can be used to determine if is a tautology; that is, it always evaluates to TRUE. If this is the case, then the program always conforms to the specification.[23]

SAT solvers

[edit]

A SAT solver is a program that can solve the Boolean satisfiability problem, the problem of finding an assignment of variables that makes a given propositional formula evaluate to true. If a Boolean formula expresses that a specific execution of a program conforms to the specification, then determining that is unsatisfiable is equivalent to determining that all executions conform to the specification. SAT solvers are often used in bounded model checking, but can also be used in unbounded model checking.[24]

Satisfiability modulo theories

[edit]

Satisfiability modulo theories (SMT) generalises Boolean satisfiability to formulas interpreted over background theories such as fixed-width bit vectors, linear arithmetic, arrays, algebraic data types and uninterpreted functions.[25] Because those theories correspond closely to the constructs of real programming languages, SMT solvers such as Z3 and cvc5 have become the automation engine behind most contemporary deductive verifiers, as well as behind symbolic execution and program synthesis tools.[26]

Deductive program verification

[edit]

Deductive verifiers translate an annotated program into verification conditions using a predicate transformer such as the weakest precondition, and then discharge those conditions with automated provers.[19] Intermediate verification languages, among them Boogie, Why3 and Viper, allow several front ends to share a single verification-condition generator and solver interface.[27] Tools of this kind include Dafny,[28] Frama-C, SPARK, VeriFast and F*.

Separation logic extends this style of reasoning to programs that manipulate pointers and the heap, by making the disjointness of memory regions part of the assertion language.[29] It underpins both interactive frameworks for verifying low-level code and automatic analysers that run on very large code bases.[30]

Applications

[edit]

Formal methods are applied in different areas of hardware and software, including routers, Ethernet switches, routing protocols, security applications, and operating system microkernels such as seL4. There are several examples in which they have been used to verify the functionality of the hardware and software used in data centres. AMD has used the ACL2 theorem prover to verify the floating-point hardware of its x86 processors, a practice established in the 1990s and carried through successive microarchitectures.[31] Intel uses such methods to verify its hardware and firmware (permanent software programmed into a read-only memory)[citation needed]. Dansk Datamatik Center used formal methods in the 1980s to develop a compiler system for the Ada programming language that went on to become a long-lived commercial product.[32][33]

There are several other projects of NASA in which formal methods are applied, such as Next Generation Air Transportation System[citation needed], Unmanned Aircraft System integration in National Airspace System,[34] and Airborne Coordinated Conflict Resolution and Detection (ACCoRD).[35] B-Method with Atelier B,[36] is used to develop safety automatisms for the various subways installed throughout the world by Alstom and Siemens, and also for Common Criteria certification and the development of system models by ATMEL and STMicroelectronics.

Formal verification has been frequently used in hardware by most of the well-known hardware vendors, such as IBM, Intel, and AMD. There are many areas of hardware, where Intel have used formal methods to verify the working of the products, such as parameterized verification of cache-coherent protocol,[37] Intel Core i7 processor execution engine validation[38] (using theorem proving, BDDs, and symbolic evaluation), optimization for Intel IA-64 architecture using HOL light theorem prover,[39] and verification of high-performance dual-port gigabit Ethernet controller with support for PCI express protocol and Intel advance management technology using Cadence.[40] Similarly, IBM has used formal methods in the verification of power gates,[41] registers,[42] and functional verification of the IBM Power7 microprocessor.[43]

Since the late 2000s, entire software systems have been verified rather than individual components. The seL4 microkernel carries a machine-checked proof that its C implementation refines an abstract specification of its behaviour, the first such proof for a general-purpose operating system kernel.[44] CompCert is an optimising C compiler accompanied by a mechanised proof that compilation preserves the semantics of the source program;[45] a randomised testing campaign that uncovered hundreds of defects in other C compilers found none in its verified components.[46] Verified cryptographic code from the HACL* and Fiat-Cryptography projects has been deployed in widely used software, including Mozilla's Network Security Services and the Linux kernel.[47][48]

Formal methods are also applied at scale outside certification regimes. Amazon Web Services has reported using TLA+ to find design defects in its distributed systems before implementation,[49] and applies automated reasoning in customer-facing services that answer security questions such as whether an access-control policy could permit public access.[50] Microsoft's SLAM project produced the Static Driver Verifier distributed with the Windows Driver Kit,[51] the Astrée analyser has been used to establish the absence of run-time errors in Airbus fly-by-wire control software,[52] and separation-logic analysers are run continuously on code bases of tens of millions of lines.[30] Vendors of instruction set architectures, including Arm and RISC-V, now publish machine-readable formal specifications that can be executed and used for verification and test generation.[53]

In software development

[edit]

In software development, formal methods are mathematical approaches to solving software (and hardware) problems at the requirements, specification, and design levels. Formal methods are most likely to be applied to safety-critical or security-critical software and systems, such as avionics software. Safety and security assurance standards permit or require their use. In civil avionics, RTCA DO-333 defines how formal methods may be used to satisfy the objectives of DO-178C,[54] and the Common Criteria call for semi-formal and formal specification and design at their highest evaluation assurance levels.[55]

For sequential software, examples of formal methods include the B-Method, the specification languages used in automated theorem proving, RAISE, and the Z notation.

In functional programming, property-based testing has allowed the mathematical specification and testing (if not exhaustive testing) of the expected behaviour of individual functions.

The Object Constraint Language (and specializations such as Java Modeling Language) has allowed object-oriented systems to be formally specified, if not necessarily formally verified.

For concurrent software and systems, Petri nets, process algebra, and finite-state machines (which are based on automata theory; see also virtual finite state machine or event driven finite state machine) allow executable software specification and can be used to build up and validate application behaviour.

Another approach to formal methods in software development is to write a specification in some form of logic—usually a variation of first-order logic—and then to directly execute the logic as though it were a program. The OWL language, based on description logic, is an example. There is also work on mapping some version of English (or another natural language) automatically to and from logic, as well as executing the logic directly. Examples are Attempto Controlled English, and Internet Business Logic, which do not seek to control the vocabulary or syntax. A feature of systems that support bidirectional English–logic mapping and direct execution of the logic is that they can be made to explain their results, in English, at the business or scientific level.[citation needed]

Semi-formal methods

[edit]

Semi-formal methods are formalisms and languages that are not considered fully "formal". It defers the task of completing the semantics to a later stage, which is then done either by human interpretation or by interpretation through software like code or test case generators.[56]

Some practitioners believe that the formal methods community has overemphasized full formalization of a specification or design.[57][58] They contend that the expressiveness of the languages involved, as well as the complexity of the systems being modelled, make full formalization a difficult and expensive task. As an alternative, various lightweight formal methods, which emphasize partial specification and focused application, have been proposed. Examples of this lightweight approach to formal methods include the Alloy object modelling notation,[59] Denney's synthesis of some aspects of the Z notation with use case driven development,[60] and the CSK VDM Tools.[61]

Lightweight approaches of this kind have since been reported at industrial scale, notably in the use of specification languages such as TLA+ to check the designs of large distributed systems before they are implemented.[49]

Formal methods and notations

[edit]

There are a variety of formal methods and notations available.

Specification languages

[edit]

Proof assistants

[edit]

Model checkers

[edit]
  • CBMC – a bounded model checker for C, C++ and Java programs
  • ESBMC[62]
  • FizzBee[63]
  • Java Pathfinder – an explicit-state model checker for Java bytecode
  • MALPAS Software Static Analysis Toolset – an industrial-strength model checker used for formal proof of safety-critical systems
  • NuSMV and nuXmv – symbolic model checkers for finite- and infinite-state systems
  • PAT – a free model checker, simulator and refinement checker for concurrent systems and CSP extensions (e.g., shared variables, arrays, fairness)
  • PRISM – a probabilistic model checker
  • SPIN
  • TLC – the explicit-state model checker for TLA+
  • UPPAAL

Solvers and competitions

[edit]

Many problems in formal methods are NP-hard, but can be solved in cases arising in practice. For example, the Boolean satisfiability problem is NP-complete by the Cook–Levin theorem, but SAT solvers can solve a variety of large instances. There are "solvers" for a variety of problems that arise in formal methods, and there are many periodic competitions to evaluate the state-of-the-art in solving such problems.[64]

Organizations

[edit]

See also

[edit]

References

[edit]
  1. ↑ Butler, R. W. (2001-08-06). "What is Formal Methods?". Retrieved 2006-11-16.
  2. ↑ Holloway, C. Michael (27–30 October 1997). "Why Engineers Should Consider Formal Methods" (PDF). 16th Digital Avionics Systems Conference. Archived from the original (PDF) on 16 November 2006. Retrieved 2006-11-16.
  3. ↑ Monin, pp.3-4
  4. ↑ Turing, A. M. (1949). "Checking a large routine". Report of a Conference on High Speed Automatic Calculating Machines. University Mathematical Laboratory, Cambridge. pp. 67–69.
  5. ↑ Floyd, Robert W. (1967). "Assigning meanings to programs". Proceedings of Symposia in Applied Mathematics. Vol. 19. American Mathematical Society. pp. 19–32.
  6. ↑ Hoare, C. A. R. (1969). "An axiomatic basis for computer programming". Communications of the ACM. 12 (10): 576–580. doi:10.1145/363235.363259.
  7. ↑ Dijkstra, Edsger W. (1975). "Guarded commands, nondeterminacy and formal derivation of programs". Communications of the ACM. 18 (8): 453–457. doi:10.1145/360933.360975.
  8. ↑ Pnueli, Amir (1977). "The temporal logic of programs". 18th Annual Symposium on Foundations of Computer Science. pp. 46–57. doi:10.1109/SFCS.1977.32.
  9. ↑ Burch, J. R.; Clarke, E. M.; McMillan, K. L.; Dill, D. L.; Hwang, L. J. (1992). "Symbolic model checking: 1020 states and beyond". Information and Computation. 98 (2): 142–170. doi:10.1016/0890-5401(92)90017-A.
  10. ↑ Biere, Armin; Cimatti, Alessandro; Clarke, Edmund; Zhu, Yunshan (1999). "Symbolic Model Checking without BDDs". Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Vol. 1579. Springer. pp. 193–207. doi:10.1007/3-540-49059-0_14.
  11. ↑ Woodcock, Jim; Larsen, Peter Gorm; Bicarregui, Juan; Fitzgerald, John (2009). "Formal methods: Practice and experience". ACM Computing Surveys. 41 (4): 1–36. doi:10.1145/1592434.1592436.
  12. ↑ Utting, Mark; Reeves, Steve (August 31, 2001). "Teaching formal methods lite via testing". Software Testing, Verification and Reliability. 11 (3): 181–195. doi:10.1002/stvr.223.
  13. ↑ Backus, J.W. (1959). "The Syntax and Semantics of the Proposed International Algebraic Language of Zürich ACM-GAMM Conference". Proceedings of the International Conference on Information Processing. UNESCO.
  14. ↑ Knuth, Donald E. (1964), Backus Normal Form vs Backus Naur Form. Communications of the ACM, 7(12):735–736.
  15. ↑ O'Hearn, Peter W.; Tennent, Robert D. (1997). Algol-like Languages.
  16. ↑ Gulwani, Sumit; Polozov, Oleksandr; Singh, Rishabh (2017). "Program Synthesis". Foundations and Trends in Programming Languages. 4 (1–2): 1–119. doi:10.1561/2500000010.
  17. ↑ Gleirscher, Mario; Marmsoler, Diego (November 2020). "Formal methods in dependable systems engineering: a survey of professionals from Europe and North America". Empirical Software Engineering. 25 (6): 4473–4546. arXiv:1812.08815. doi:10.1007/s10664-020-09836-5. ISSN 1573-7616. Retrieved 2026-05-16.
  18. ↑ Geuvers, Herman (2009). "Proof assistants: History, ideas and future". Sādhanā. 34 (1): 3–25. doi:10.1007/s12046-009-0001-5.
  19. 1 2 Filliâtre, Jean-Christophe (2011). "Deductive software verification". International Journal on Software Tools for Technology Transfer. 13 (5): 397–403. doi:10.1007/s10009-011-0211-0.
  20. ↑ A. Cortesi and M. Zanioli, Widening and Narrowing Operators for Abstract Interpretation Archived 2015-09-23 at the Wayback Machine. Computer Languages, Systems and Structures. Volume 37(1), pp. 24–42, Elsevier, ISSN 1477-8424 (2011).
  21. ↑ Bjørner, Dines; Henson, Martin C. (2008). Logics of Specification Languages. pp. VII–XI.
  22. ↑ Bryant, Randal E. (2018). "Binary Decision Diagrams". In Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut; Bloem, Roderick (eds.). Handbook of Model Checking. p. 191.
  23. ↑ Chaki, Sagar; Gurfinkel, Arie (2018). "BDD-Based Symbolic Model Checking". In Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut; Bloem, Roderick (eds.). Handbook of Model Checking. p. 191.
  24. ↑ Prasad, Mukul R; Biere, Armin; Gupta, Aarti (January 25, 2005). "A survey of recent advances in SAT-based formal verification". International Journal on Software Tools for Technology Transfer. 7 (2): 156–173. doi:10.1007/s10009-004-0183-4.
  25. ↑ Barrett, Clark; Tinelli, Cesare (2018). "Satisfiability Modulo Theories". Handbook of Model Checking. Springer. pp. 305–343. doi:10.1007/978-3-319-10575-8_11.
  26. ↑ de Moura, Leonardo; Bjørner, Nikolaj (2008). "Z3: An Efficient SMT Solver". Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Vol. 4963. Springer. pp. 337–340. doi:10.1007/978-3-540-78800-3_24.
  27. ↑ Filliâtre, Jean-Christophe; Paskevich, Andrei (2013). "Why3 — Where Programs Meet Provers". Programming Languages and Systems. Lecture Notes in Computer Science. Vol. 7792. Springer. pp. 125–128. doi:10.1007/978-3-642-37036-6_8.
  28. ↑ Leino, K. Rustan M. (2010). "Dafny: An Automatic Program Verifier for Functional Correctness". Logic for Programming, Artificial Intelligence, and Reasoning. Lecture Notes in Computer Science. Vol. 6355. Springer. pp. 348–370. doi:10.1007/978-3-642-17511-4_20.
  29. ↑ Reynolds, John C. (2002). "Separation logic: a logic for shared mutable data structures". Proceedings 17th Annual IEEE Symposium on Logic in Computer Science. pp. 55–74. doi:10.1109/LICS.2002.1029817.
  30. 1 2 Distefano, Dino; Fähndrich, Manuel; Logozzo, Francesco; O'Hearn, Peter W. (2019). "Scaling static analyses at Facebook". Communications of the ACM. 62 (8): 62–70. doi:10.1145/3338112.
  31. ↑ Russinoff, David M. (2019). Formal Verification of Floating-Point Hardware Design: A Mathematical Approach. Springer. doi:10.1007/978-3-319-95513-1. ISBN 978-3-319-95512-4.
  32. ↑ Bjørner, Dines; Gram, Christian; Oest, Ole N.; Rystrøm, Leif (2011). "Dansk Datamatik Center". In Impagliazzo, John; Lundin, Per; Wangler, Benkt (eds.). History of Nordic Computing 3: IFIP Advances in Information and Communication Technology. Springer. pp. 350–359.
  33. ↑ Bjørner, Dines; Havelund, Klaus. "40 Years of Formal Methods: Some Obstacles and Some Possibilities?". FM 2014: Formal Methods: 19th International Symposium, Singapore, May 12–16, 2014. Proceedings (PDF). Springer. pp. 42–61.
  34. ↑ Gheorghe, A. V., & Ancel, E. (2008, November). Unmanned aerial systems integration to National Airspace System. In Infrastructure Systems and Services: Building Networks for a Brighter Future (INFRA), 2008 First International Conference on (pp. 1-5). IEEE.
  35. ↑ Airborne Coordinated Conflict Resolution and Detection, http://shemesh.larc.nasa.gov/people/cam/ACCoRD/ Archived 2016-03-05 at the Wayback Machine
  36. ↑ "Atelier B". www.atelierb.eu.
  37. ↑ C. T. Chou, P. K. Mannava, S. Park, "A simple method for parameterized verification of cache coherence protocols", Formal Methods in Computer-Aided Design, pp. 382–398, 2004.
  38. ↑ Formal Verification in Intel Core i7 Processor Execution Engine Validation, http://cps-vo.org/node/1371 Archived 2015-05-03 at the Wayback Machine, accessed at September 13, 2013.
  39. ↑ J. Grundy, "Verified optimizations for the Intel IA-64 architecture", In Theorem Proving in Higher Order Logics, Springer Berlin Heidelberg, 2004, pp. 215–232.
  40. ↑ E. Seligman, I. Yarom, "Best known methods for using Cadence Conformal LEC", at Intel.
  41. ↑ C. Eisner, A. Nahir, K. Yorav, "Functional verification of power gated designs by compositional reasoning[dead link]", Computer Aided Verification, Springer Berlin Heidelberg, pp. 433–445.
  42. ↑ P. C. Attie, H. Chockler, "Automatic verification of fault-tolerant register emulations", Electronic Notes in Theoretical Computer Science, vol. 149, no. 1, pp. 49–60.
  43. ↑ K. D. Schubert, W. Roesner, J. M. Ludden, J. Jackson, J. Buchert, V. Paruthi, B. Brock, "Functional verification of the IBM POWER7 microprocessor and POWER7 multiprocessor systems", IBM Journal of Research and Development, vol. 55, no 3.
  44. ↑ Klein, Gerwin; et al. (2009). "seL4: formal verification of an OS kernel". Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles. pp. 207–220. doi:10.1145/1629575.1629596.
  45. ↑ Leroy, Xavier (2009). "Formal verification of a realistic compiler". Communications of the ACM. 52 (7): 107–115. doi:10.1145/1538788.1538814.
  46. ↑ Yang, Xuejun; Chen, Yang; Eide, Eric; Regehr, John (2011). "Finding and understanding bugs in C compilers". Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 283–294. doi:10.1145/1993498.1993532.
  47. ↑ Zinzindohoué, Jean-Karim; et al. (2017). "HACL*: A Verified Modern Cryptographic Library". Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security. pp. 1789–1806. doi:10.1145/3133956.3134043.
  48. ↑ Erbsen, Andres; et al. (2019). "Simple High-Level Code for Cryptographic Arithmetic – With Proofs, Without Compromises". 2019 IEEE Symposium on Security and Privacy. pp. 1202–1219. doi:10.1109/SP.2019.00005. hdl:1721.1/130000.
  49. 1 2 Newcombe, Chris; et al. (2015). "How Amazon Web Services uses formal methods". Communications of the ACM. 58 (4): 66–73. doi:10.1145/2699417.
  50. ↑ Cook, Byron (2018). "Formal Reasoning About the Security of Amazon Web Services". Computer Aided Verification. Lecture Notes in Computer Science. Vol. 10981. Springer. pp. 38–47. doi:10.1007/978-3-319-96145-3_3.
  51. ↑ Ball, Thomas; Levin, Vladimir; Rajamani, Sriram K. (2011). "A decade of software model checking with SLAM". Communications of the ACM. 54 (7): 68–76. doi:10.1145/1965724.1965743.
  52. ↑ Blanchet, Bruno; et al. (2003). "A static analyzer for large safety-critical software". Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation. pp. 196–207. arXiv:cs/0701193. doi:10.1145/781131.781153.
  53. ↑ Armstrong, Alasdair; et al. (2019). "ISA semantics for ARMv8-A, RISC-V, and CHERI-MIPS". Proceedings of the ACM on Programming Languages. 3 (POPL): 1–31. doi:10.1145/3290384. hdl:20.500.11820/87eb0085-0bbf-4987-b540-6661ee0dc353.
  54. ↑ DO-333: Formal Methods Supplement to DO-178C and DO-278A. RTCA. 2011.
  55. ↑ Common Criteria for Information Technology Security Evaluation, Part 3: Security Assurance Components. 2022.
  56. ↑ X2R-2, deliverable D5.1.
  57. ↑ Daniel Jackson and Jeannette Wing, "Lightweight Formal Methods", IEEE Computer, April 1996
  58. ↑ Vinu George and Rayford Vaughn, "Application of Lightweight Formal Methods in Requirement Engineering" Archived 2006-03-01 at the Wayback Machine, Crosstalk: The Journal of Defense Software Engineering, January 2003
  59. ↑ Daniel Jackson, "Alloy: A Lightweight Object Modelling Notation", ACM Transactions on Software Engineering and Methodology (TOSEM), Volume 11, Issue 2 (April 2002), pp. 256-290
  60. ↑ Richard Denney, Succeeding with Use Cases: Working Smart to Deliver Quality, Addison-Wesley Professional Publishing, 2005, ISBN 0-321-31643-6.
  61. ↑ Sten Agerholm and Peter G. Larsen, "A Lightweight Approach to Formal Methods" Archived 2006-03-09 at the Wayback Machine, In Proceedings of the International Workshop on Current Trends in Applied Formal Methods, Boppard, Germany, Springer-Verlag, October 1998
  62. ↑ "ESBMC". esbmc.org.
  63. ↑ "FizzBee". fizzbee.io.
  64. ↑ Bartocci, Ezio; Beyer, Dirk; Black, Paul E.; Fedyukovich, Grigory; Garavel, Hubert; Hartmanns, Arnd; Huisman, Marieke; Kordon, Fabrice; Nagele, Julian; Sighireanu, Mihaela; Steffen, Bernhard; Suda, Martin; Sutcliffe, Geoff; Weber, Tjark; Yamada, Akihisa (2019). "TOOLympics 2019: An Overview of Competitions in Formal Methods". In Beyer, Dirk; Huisman, Marieke; Kordon, Fabrice; Steffen, Bernhard (eds.). Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Cham: Springer International Publishing. pp. 3–24. doi:10.1007/978-3-030-17502-3_1. ISBN 978-3-030-17502-3.
  65. ↑ Froleyks, Nils; Heule, Marijn; Iser, Markus; Järvisalo, Matti; Suda, Martin (2021-12-01). "SAT Competition 2020". Artificial Intelligence. 301 103572. doi:10.1016/j.artint.2021.103572. hdl:10138/335114. ISSN 0004-3702.
  66. ↑ Cornejo, César (2021-01-27). "SAT-based arithmetic support for alloy". Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering. ASE '20. New York, NY, USA: Association for Computing Machinery. pp. 1161–1163. doi:10.1145/3324884.3415285. ISBN 978-1-4503-6768-4.
  67. ↑ Barrett, Clark; Deters, Morgan; de Moura, Leonardo; Oliveras, Albert; Stump, Aaron (2013-03-01). "6 Years of SMT-COMP". Journal of Automated Reasoning. 50 (3): 243–277. doi:10.1007/s10817-012-9246-5. ISSN 1573-0670.
  68. ↑ Fedyukovich, Grigory; Rümmer, Philipp (2021-09-13). "Competition Report: CHC-COMP-21". Electronic Proceedings in Theoretical Computer Science. 344: 91–108. arXiv:2008.02939. doi:10.4204/EPTCS.344.7. ISSN 2075-2180.
  69. ↑ Shukla, Ankit; Biere, Armin; Pulina, Luca; Seidl, Martina (November 2019). "A Survey on Applications of Quantified Boolean Formulas". 2019 IEEE 31st International Conference on Tools with Artificial Intelligence (ICTAI). IEEE. pp. 78–84. doi:10.1109/ICTAI.2019.00020. ISBN 978-1-7281-3798-8.
  70. ↑ Pulina, Luca; Seidl, Martina (2019-09-01). "The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)". Artificial Intelligence. 274: 224–248. doi:10.1016/j.artint.2019.04.002. ISSN 0004-3702.
  71. ↑ Beyer, Dirk (2022). "Progress on Software Verification: SV-COMP 2022". In Fisman, Dana; Rosu, Grigore (eds.). Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Vol. 13244. Cham: Springer International Publishing. pp. 375–402. doi:10.1007/978-3-030-99527-0_20. ISBN 978-3-030-99527-0.
  72. ↑ Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2017-11-28). "SyGuS-Comp 2017: Results and Analysis". Electronic Proceedings in Theoretical Computer Science. 260: 97–115. arXiv:1611.07627. doi:10.4204/EPTCS.260.9. ISSN 2075-2180.

Further reading

[edit]
[edit]
Archival material
Retrieved from "https://en.wikipedia.org/w/index.php?title=Formal_methods&oldid=1373666187"