Precise verification of C programs

Precise verification of C programs

<p>Most current approaches to software verification are one-sided -- a safety prover will try to prove that a program is safe, while a bug-finding tool will try to find bugs. It is rare to find an analyser that is optimised for both tasks, which is problematic since it is hard to know in adva...

Bibliografske podrobnosti
Glavni avtor:	Lewis, M
Drugi avtorji:	Kroening, D
Format:	Thesis
Jezik:	English
Izdano:	2014
Teme:	Theory and automated verification

Podobne knjige/članki

Automated quantitative software verification
od: Kattenbelt, M
Izdano: (2010)

Quantitative verification of real-time properties with application to medical devices
od: Marco Diciolla, M, et al.
Izdano: (2014)

Monotonicity in shared-memory program verification
od: Kaiser, A
Izdano: (2013)

Intersection types and higer-order model checking
od: Ramsay, S, et al.
Izdano: (2014)

Forward looking logics and automata
od: Ley, C
Izdano: (2011)

Probabilistic guarded commands mechanized in HOL
od: Hurd, J, et al.
Izdano: (2005)

Incremental modelling for verified communication architectures
od: Boehm, P, et al.
Izdano: (2011)

Game semantics based equivalence checking of higher-order programs
od: Hopkins, D, et al.
Izdano: (2012)

Partial correctness for probabilistic demonic programs
od: McIver, A, et al.
Izdano: (2001)

Automated Verification of Building Components Using BIM Models and Point Clouds
od: Honti Richard, et al.
Izdano: (2020-09-01)

Verification of asynchronous concurrency and the shaped stack constraint
od: Kochems, J
Izdano: (2014)

Abstraction discovery and refinement for model checking by symbolic trajectory evaluation
od: Adams, S
Izdano: (2014)

Predicate Abstraction of ANSI-C Programs Using SAT
od: Clarke, E, et al.
Izdano: (2004)

Automation Processes for Efficient Verification of Complex Systems: An Empirical Case Study
od: Rune Andre Haugen, et al.
Izdano: (2024-12-01)

Functions with local state: regularity and undecidability
od: Murawski, A
Izdano: (2005)

An algebraic theory of componentised interaction
od: Chilton, C
Izdano: (2013)

On learning assumptions for compositional verification of probabilistic systems
od: Feng, L
Izdano: (2014)

Program analysis with interpolants
od: Weissenbacher, G, et al.
Izdano: (2010)

C Program Verification: VC Explanation and the Standard Library
od: A. V. Promsky
Izdano: (2011-12-01)

Criticality Analysis for the Verification and Validation of Automated Vehicles
od: Christian Neurohr, et al.
Izdano: (2021-01-01)

Techniques and tools for the verification of concurrent systems
od: Palikareva, H
Izdano: (2012)

Repairing strings and trees
od: Riveros Jaeger, C
Izdano: (2013)

An interpolating decision procedure for transitive relations with uninterpreted functions
od: Kroening, D, et al.
Izdano: (2009)

Verification of the expert’s opinion
od: M. H. Shcherbakovskyi, et al.
Izdano: (2022-09-01)

A New Method for Verification and Evaluation of PLC Software
od: Muhammed Ali Nur ÖZ, et al.
Izdano: (2023-06-01)

Abstract satisfaction
od: Haller, L
Izdano: (2013)

Coverage Fulfillment Automation in Hardware Functional Verification Using Genetic Algorithms
od: Gabriel Mihail Danciu, et al.
Izdano: (2022-01-01)

On Construction and Verification of PLC-Programs
od: E. V. Kuzmin, et al.
Izdano: (2015-02-01)

Higher-order semantics for quantum programming languages with classical control
od: Atzemoglou, GP
Izdano: (2012)

Explainability of Automated Fact Verification Systems: A Comprehensive Review
od: Manju Vallayil, et al.
Izdano: (2023-11-01)

Verificator: Educational Tool for Learning Programming
od: Danijel RADOSEVIC, et al.
Izdano: (2009-10-01)

Program synthesis from domain specific object models
od: Faitelson, D
Izdano: (2008)

Wall Structure Geometry Verification Using TLS Data and BIM Model
od: Gabriela Bariczová, et al.
Izdano: (2021-12-01)

Testimony on Voter Verification
od: Selker, Ted
Izdano: (2015)

EL-ifying ontologies
od: Carral, D, et al.
Izdano: (2014)

Static analyses over weak memory
od: Nimal, V, et al.
Izdano: (2014)

Pushing the boundaries of tractable ontology reasoning
od: Carral, D, et al.
Izdano: (2014)

Reinforcement Learning Made Affordable for Hardware Verification Engineers
od: Alexandru Dinu, et al.
Izdano: (2022-11-01)

Tractable query answering for description logics via query rewriting
od: Perez-Urbina, H, et al.
Izdano: (2010)

Automation of Formal Veriﬁcation of Programs in the Pifagor Language
od: M. S. Ushakova, et al.
Izdano: (2015-08-01)