Introducing software verification with Dafny language : proving program correctness

Book Cover
Average Rating
Published
Berkeley, CA : Apress L. P., 2022.
Status
Available Online

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

Also in this Series

Checking series information...

More Like This

Loading more titles like this title...

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. 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 Apress L. P, 2022.

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
Go To Grouped Work View in Staff Client

Grouping Information

Grouped Work IDa6b101ee-ea8f-ce81-4632-1f057867f19c-eng
Full titleintroducing software verification with dafny language proving program correctness
Authorsitnikovski boro
Grouping Categorybook
Last Update2024-06-04 09:42:47AM
Last Indexed2024-09-28 02:32:51AM

Book Cover Information

Image SourcecontentCafe
First LoadedMar 23, 2023
Last UsedSep 27, 2024

Marc Record

First DetectedMar 20, 2023 10:17:00 AM
Last File Modification TimeMar 20, 2023 10:17:00 AM
SuppressedRecord had no items

MARC Record

LEADER03768cam a2200481Ii 4500
001on1301900058
003OCoLC
00520230320101519.0
006m     o  d        
007cr |n|||||||||
008220304s2022    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.)
0247 |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
049 |a MAIN
050 4|a QA76.76.V47|b S58 2022
072 7|a COM000000|2 bisacsh
08204|a 005.1/4|2 23
1001 |a Sitnikovski, Boro,|e author.
24510|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.
300 |a 1 online resource (144 pages) :|b 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.
5050 |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
650 4|a Dafny (Computer program language).
77608|c Original|z 1484279778|z 9781484279779|w (OCoLC)1287920026
85640|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