Nyhet

Rigorous Software Development

An Introduction to Program Verification

AvJosé Bacelar Almeida,Maria João Frade

Häftad, Engelska, 2026

Del i serien Undergraduate Topics in Computer Science

672 kr

Beställningsvara. Skickas inom 10-15 vardagar. Fri frakt över 249 kr.

Fler format och utgåvor

Häftad

440 kr

Beskrivning

Software errors can lead to catastrophic consequences, from financial losses to threats to human safety. As a result, rigorous methods for software development and validation have become increasingly critical. Program verification, a key area of formal methods, provides mathematical tools and techniques to ensure that software behaves as intended. This book provides a comprehensive introduction to program verification, combining theoretical foundations with practical applications using real-world tools. It offers a self-contained overview of propositional logic and first-order reasoning with theories, followed by a study of Hoare-style program logic with annotations and the generation of verification conditions. The use of Frama-C’s WP plug-in for verifying C programs annotated with the ACSL specification language, including safety properties, is also covered. This revised and expanded second edition incorporates recent advances in formal methods and program verification, integrating new techniques, tools, and exercises to equip readers with the skills necessary for rigorous software development.Rigorous Software Development is ideal for computer science students, researchers in formal methods, and software engineers seeking a deeper understanding of program verification techniques and tools. It equips readers with the knowledge needed to apply rigorous methods in practice while providing a solid foundation for the evolving landscape of modern software engineering.

Produktinformation

Utgivningsdatum:2026-05-24
Mått:155 x 235 x 17 mm
Vikt:470 g
Format:Häftad
Språk:Engelska
Serie:Undergraduate Topics in Computer Science
Antal sidor:291
Upplaga:2
Förlag:Springer London Ltd
ISBN:9781447175575

Utforska kategorier

Programvaruutveckling inom Data och IT
Systemvetenskap och AI inom Data och IT

Mer om författaren

José Bacelar Almeida is a lecturer at the University of Minho, Portugal. He graduated in Electrical and Computer Engineering and received his PhD in Computer Science from the University of Minho. His areas of interest include semantics of programming languages, proof assistants, and security. Maria João Frade obtained her PhD in Computer Science from the University of Minho, Portugal, and is currently a lecturer at this institution. Her research interests include type theory, structural proof theory, semantics of programming languages and program logics. Jorge Sousa Pinto obtained his PhD in Computer Science from École Polytechnique, France, and is currently a lecturer at the University of Minho, Portugal. His interests include program verification and the use of formal methods in software engineering. Simão Melo de Sousa is a lecturer at the University of Beira Interior, Portugal. He graduated in Computer Science from the University of Orléans, France, and received his PhD in ComputerScience from the University of Nice-Sophia Antipolis / INRIA. His interests include formal methods, reliability and security of computer systems, and computer-aided reasoning.

Innehållsförteckning

List of Figures.- 1. Introduction.- 2. An Overview of Formal Methods Tools and Techniques.- 3. Propositional Logic.- 4. First-Order Logic.- 5. Hoare Logic.- 6. Generating Verification Conditions.- 7. Safety Properties.- 8. Procedures and Contracts.- 9. Specifying C Programs.- 10. Verifying C Programs.- Bibliography.- Index.