*Jeremy Avigad*

- Published in print:
- 2008
- Published Online:
- February 2010
- ISBN:
- 9780199296453
- eISBN:
- 9780191711961
- Item type:
- chapter

- Publisher:
- Oxford University Press
- DOI:
- 10.1093/acprof:oso/9780199296453.003.0013
- Subject:
- Philosophy, Logic/Philosophy of Mathematics

In informal speech, ascriptions of mathematical understanding are typically clarified by spelling out the kinds of abilities an agent is assumed to possess. This chapter argues that such an approach ...
More

In informal speech, ascriptions of mathematical understanding are typically clarified by spelling out the kinds of abilities an agent is assumed to possess. This chapter argues that such an approach is fruitful in scientific domains as well. The practice of formal verification, which involves the use of computers to check mathematical proofs, is one example. In particular, understanding ordinary mathematical proofs involves being able to recognize interesting classes of high-level inferences.Less

In informal speech, ascriptions of mathematical understanding are typically clarified by spelling out the kinds of abilities an agent is assumed to possess. This chapter argues that such an approach is fruitful in scientific domains as well. The practice of formal verification, which involves the use of computers to check mathematical proofs, is one example. In particular, understanding ordinary mathematical proofs involves being able to recognize interesting classes of high-level inferences.

*Pierre-Loïc Garoche*

- Published in print:
- 2019
- Published Online:
- January 2020
- ISBN:
- 9780691181301
- eISBN:
- 9780691189581
- Item type:
- chapter

- Publisher:
- Princeton University Press
- DOI:
- 10.23943/princeton/9780691181301.003.0002
- Subject:
- Mathematics, Applied Mathematics

This chapter gives a brief overview of some formal methods and their use in the context of critical embedded systems development. While testing is a common practice for a lot of engineers as a way to ...
More

This chapter gives a brief overview of some formal methods and their use in the context of critical embedded systems development. While testing is a common practice for a lot of engineers as a way to evaluate whether the program they developed fulfills its needs, formal methods are less known and may require a little introduction to the non-expert. This chapter thus serves as a reasonable introduction to the control expert engineer. It first defines the semantics of programs: their basic properties and their meaning. Then, the chapter outlines different formal verifications and explains how they reason on the program artifact. A last part addresses the soundness of the analyses with respect to the actual semantics.Less

This chapter gives a brief overview of some formal methods and their use in the context of critical embedded systems development. While testing is a common practice for a lot of engineers as a way to evaluate whether the program they developed fulfills its needs, formal methods are less known and may require a little introduction to the non-expert. This chapter thus serves as a reasonable introduction to the control expert engineer. It first defines the semantics of programs: their basic properties and their meaning. Then, the chapter outlines different formal verifications and explains how they reason on the program artifact. A last part addresses the soundness of the analyses with respect to the actual semantics.