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...

Descripció completa

Dades bibliogràfiques
Autor principal:	Lewis, M
Altres autors:	Kroening, D
Format:	Thesis
Idioma:	English
Publicat:	2014
Matèries:	Theory and automated verification

Ítems similars

Automated quantitative software verification
per: Kattenbelt, M
Publicat: (2010)

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

Monotonicity in shared-memory program verification
per: Kaiser, A
Publicat: (2013)

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

Forward looking logics and automata
per: Ley, C
Publicat: (2011)

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

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

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

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

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

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

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

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

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

Functions with local state: regularity and undecidability
per: Murawski, A
Publicat: (2005)

An algebraic theory of componentised interaction
per: Chilton, C
Publicat: (2013)

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

Program analysis with interpolants
per: Weissenbacher, G, et al.
Publicat: (2010)

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

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

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

Repairing strings and trees
per: Riveros Jaeger, C
Publicat: (2013)

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

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

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

Abstract satisfaction
per: Haller, L
Publicat: (2013)

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

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

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

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

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

Program synthesis from domain specific object models
per: Faitelson, D
Publicat: (2008)

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

Testimony on Voter Verification
per: Selker, Ted
Publicat: (2015)

EL-ifying ontologies
per: Carral, D, et al.
Publicat: (2014)

Static analyses over weak memory
per: Nimal, V, et al.
Publicat: (2014)

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

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

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

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