Qed at Large: Przegląd inżynierii formalnie zweryfikowanego oprogramowania

Oryginalny tytuł:

Qed at Large: A Survey of Engineering of Formally Verified Software

Zawartość książki:

Opracowanie formalnych dowodów poprawności programów może zwiększyć rzeczywistą i postrzeganą niezawodność oraz ułatwić lepsze zrozumienie specyfikacji programów i ich podstawowych założeń. Narzędzia wspierające taki rozwój są dostępne od ponad 40 lat, ale dopiero niedawno doczekały się szerokiego praktycznego zastosowania.

Projekty oparte na konstrukcji sprawdzanych maszynowo dowodów formalnych osiągają obecnie bezprecedensową skalę, porównywalną z dużymi projektami programistycznymi, co prowadzi do nowych wyzwań w zakresie opracowywania i utrzymywania dowodów. Pomimo rosnącego znaczenia, dziedzina inżynierii dowodu rzadko jest rozpatrywana samodzielnie; powiązane teorie, techniki i narzędzia obejmują wiele dziedzin i miejsc. QED at Large obejmuje oś czasu i literaturę badawczą dotyczącą tworzenia dowodów dla weryfikacji programów, w tym teorie, języki i narzędzia.

Kładzie nacisk na wyzwania i przełomy na każdym etapie historii oraz podkreśla wyzwania, które są obecnie obecne ze względu na rosnącą skalę rozwoju dowodów. Niniejsza monografia jest przeznaczona dla badaczy i studentów, którzy są nowicjuszami w tej dziedzinie.

Zapewnia ona czytelnikowi wnikliwy przegląd prac, które doprowadziły do powstania współczesnych technik formalnej weryfikacji oprogramowania. W czasach rosnącej automatyzacji jest to podstawa wielu systemów oprogramowania, więc podkreślono również przyszłe trendy.