Introducing software verification with Dafny language : proving program correctness
Description
Loading Description...
More Details
Format
Language
English
ISBN
9781484279786, 1484279786
UPC
10.1007/978-1-4842-7978-6
Notes
Bibliography
Includes bibliographical references and index.
Description
Get introduced to software verification and proving correctness using the Microsoft Research-backed programming language, Dafny. While some other books on this topic are quite mathematically rigorous, this book will use as little mathematical symbols and rigor as possible, and explain every concept using plain English. It's the perfect primer for software programmers and developers with C# and other programming language skills. Writing correct software can be hard, so you'll learn the concept of computation and software verification. Then, apply these concepts and techniques to confidently write bug-free code that is easy to understand. Source code will be available throughout the book and freely available via GitHub. After reading and using this book you'll be able write correct, big free software source code applicable no matter which platform and programming language you use. What You Will Learn Discover the Microsoft Research-backed Dafny programming language Explore Hoare logic, imperative and functional programs Work with pre- and post-conditions Use data types, pattern matching, and classes Dive into verification examples for potential re-use for your own projects Who This Book Is For Software developers and programmers with at least prior, basic programming experience. No specific language needed. It is also for those with very basic mathematical experience (function, variables).
Local note
O'Reilly,O'Reilly Online Learning: Academic/Public Library Edition
Subjects
LC Subjects
Also in this Series
Checking series information...
Reviews from GoodReads
Loading GoodReads Reviews.
Citations
APA Citation, 7th Edition (style guide)
Sitnikovski, B. (2022). Introducing software verification with Dafny language: proving program correctness . Apress L. P..
Chicago / Turabian - Author Date Citation, 17th Edition (style guide)Sitnikovski, Boro. 2022. Introducing Software Verification With Dafny Language: Proving Program Correctness. Berkeley, CA: Apress L. P.
Chicago / Turabian - Humanities (Notes and Bibliography) Citation, 17th Edition (style guide)Sitnikovski, Boro. Introducing Software Verification With Dafny Language: Proving Program Correctness Berkeley, CA: Apress L. P, 2022.
Harvard Citation (style guide)Sitnikovski, B. (2022). Introducing software verification with dafny language: proving program correctness. Berkeley, CA: Apress L. P.
MLA Citation, 9th Edition (style guide)Sitnikovski, Boro. Introducing Software Verification With Dafny Language: Proving Program Correctness Apress L. P., 2022.
Note! Citations contain only title, author, edition, publisher, and year published. Citations should be used as a guideline and should be double checked for accuracy. Citation formats are based on standards as of August 2021.
Staff View
Grouped Work ID
a6b101ee-ea8f-ce81-4632-1f057867f19c-eng
Grouping Information
| Grouped Work ID | a6b101ee-ea8f-ce81-4632-1f057867f19c-eng |
|---|---|
| Full title | introducing software verification with dafny language proving program correctness |
| Author | sitnikovski boro |
| Grouping Category | book |
| Last Update | 2025-01-24 12:33:29PM |
| Last Indexed | 2025-01-25 03:22:21AM |
Book Cover Information
| Image Source | contentCafe |
|---|---|
| First Loaded | Jan 13, 2025 |
| Last Used | Jan 13, 2025 |
Marc Record
| First Detected | Mar 20, 2023 10:17:00 AM |
|---|---|
| Last File Modification Time | Dec 17, 2024 08:18:41 AM |
| Suppressed | Record had no items |
MARC Record
| LEADER | 03760cam a2200481 i 4500 | ||
|---|---|---|---|
| 001 | on1301900058 | ||
| 003 | OCoLC | ||
| 005 | 20241217081754.0 | ||
| 006 | m o d | ||
| 007 | cr |n||||||||| | ||
| 008 | 220304s2022 caua ob 001 0 eng d | ||
| 019 | |a 1301451632|a 1301484192|a 1301770824|a 1302009289 | ||
| 020 | |a 9781484279786|q (electronic bk.) | ||
| 020 | |a 1484279786|q (electronic bk.) | ||
| 024 | 7 | |a 10.1007/978-1-4842-7978-6|2 doi | |
| 035 | |a (OCoLC)1301900058|z (OCoLC)1301451632|z (OCoLC)1301484192|z (OCoLC)1301770824|z (OCoLC)1302009289 | ||
| 037 | |a 9781484279786|b O'Reilly Media | ||
| 040 | |a YDX|b eng|c YDX|d YDX|d EBLCP|d ORMDA|d GW5XE|d OCLCO|d OCLCF|d UKAHL|d OCLCQ|d VLB|d OCLCO|d OCLCQ | ||
| 049 | |a MAIN | ||
| 050 | 4 | |a QA76.76.V47|b S58 2022eb | |
| 072 | 7 | |a COM000000|2 bisacsh | |
| 082 | 0 | 4 | |a 005.1/4|2 23 |
| 100 | 1 | |a Sitnikovski, Boro,|e author. | |
| 245 | 1 | 0 | |a Introducing software verification with Dafny language :|b proving program correctness /|c Boro Sitnikovski. |
| 264 | 1 | |a Berkeley, CA :|b Apress L. P.,|c 2022. | |
| 264 | 4 | |c ©2022 | |
| 300 | |a 1 online resource (144 pages : illustrations) | ||
| 336 | |a text|b txt|2 rdacontent | ||
| 337 | |a computer|b c|2 rdamedia | ||
| 338 | |a online resource|b cr|2 rdacarrier | ||
| 504 | |a Includes bibliographical references and index. | ||
| 505 | 0 | |a Introduction: Languages and Systems -- Chapter 1: Our First Program -- Chapter 2: Logic -- Chapter 3: Computation -- Chapter 4: Mathematical Foundations -- Chapter 5: Proofs -- Chapter 6: Specifications -- Chapter 7: Mathematical Induction -- Chapter 8: Verification Exercises -- Chapter 9: Implementing a Formal System. Conclusion -- Bibliography -- Appendix A: Godels Theorems. | |
| 520 | |a Get introduced to software verification and proving correctness using the Microsoft Research-backed programming language, Dafny. While some other books on this topic are quite mathematically rigorous, this book will use as little mathematical symbols and rigor as possible, and explain every concept using plain English. It's the perfect primer for software programmers and developers with C# and other programming language skills. Writing correct software can be hard, so you'll learn the concept of computation and software verification. Then, apply these concepts and techniques to confidently write bug-free code that is easy to understand. Source code will be available throughout the book and freely available via GitHub. After reading and using this book you'll be able write correct, big free software source code applicable no matter which platform and programming language you use. What You Will Learn Discover the Microsoft Research-backed Dafny programming language Explore Hoare logic, imperative and functional programs Work with pre- and post-conditions Use data types, pattern matching, and classes Dive into verification examples for potential re-use for your own projects Who This Book Is For Software developers and programmers with at least prior, basic programming experience. No specific language needed. It is also for those with very basic mathematical experience (function, variables). | ||
| 588 | |a Description based upon print version of record. | ||
| 590 | |a O'Reilly|b O'Reilly Online Learning: Academic/Public Library Edition | ||
| 650 | 0 | |a Computer software|x Verification.|9 34213 | |
| 776 | 0 | 8 | |c Original|z 1484279778|z 9781484279779|w (OCoLC)1287920026 |
| 856 | 4 | 0 | |u https://library.access.arlingtonva.us/login?url=https://learning.oreilly.com/library/view/~/9781484279786/?ar|x O'Reilly|z eBook |
| 938 | |a Askews and Holts Library Services|b ASKH|n AH39844352 | ||
| 938 | |a YBP Library Services|b YANK|n 17839687 | ||
| 938 | |a ProQuest Ebook Central|b EBLB|n EBL6898798 | ||
| 994 | |a 92|b VIA | ||
| 999 | |c 283493|d 283493 | ||