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

Fuld beskrivelse

Bibliografiske detaljer
Hovedforfatter:	Lewis, M
Andre forfattere:	Kroening, D
Format:	Thesis
Sprog:	English
Udgivet:	2014
Fag:	Theory and automated verification

Lignende værker

Automated quantitative software verification
af: Kattenbelt, M
Udgivet: (2010)

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

Monotonicity in shared-memory program verification
af: Kaiser, A
Udgivet: (2013)

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

Forward looking logics and automata
af: Ley, C
Udgivet: (2011)

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

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

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

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

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

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

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

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

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

Functions with local state: regularity and undecidability
af: Murawski, A
Udgivet: (2005)

An algebraic theory of componentised interaction
af: Chilton, C
Udgivet: (2013)

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

Program analysis with interpolants
af: Weissenbacher, G, et al.
Udgivet: (2010)

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

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

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

Repairing strings and trees
af: Riveros Jaeger, C
Udgivet: (2013)

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

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

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

Abstract satisfaction
af: Haller, L
Udgivet: (2013)

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

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

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

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

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

Program synthesis from domain specific object models
af: Faitelson, D
Udgivet: (2008)

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

Testimony on Voter Verification
af: Selker, Ted
Udgivet: (2015)

EL-ifying ontologies
af: Carral, D, et al.
Udgivet: (2014)

Static analyses over weak memory
af: Nimal, V, et al.
Udgivet: (2014)

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

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

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

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