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

Volledige beschrijving

Bibliografische gegevens
Hoofdauteur:	Lewis, M
Andere auteurs:	Kroening, D
Formaat:	Thesis
Taal:	English
Gepubliceerd in:	2014
Onderwerpen:	Theory and automated verification

Gelijkaardige items

Automated quantitative software verification
door: Kattenbelt, M
Gepubliceerd in: (2010)

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

Monotonicity in shared-memory program verification
door: Kaiser, A
Gepubliceerd in: (2013)

Intersection types and higer-order model checking
door: Ramsay, S, et al.
Gepubliceerd in: (2014)

Forward looking logics and automata
door: Ley, C
Gepubliceerd in: (2011)

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

Incremental modelling for verified communication architectures
door: Boehm, P, et al.
Gepubliceerd in: (2011)

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

Partial correctness for probabilistic demonic programs
door: McIver, A, et al.
Gepubliceerd in: (2001)

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

Verification of asynchronous concurrency and the shaped stack constraint
door: Kochems, J
Gepubliceerd in: (2014)

Abstraction discovery and refinement for model checking by symbolic trajectory evaluation
door: Adams, S
Gepubliceerd in: (2014)

Predicate Abstraction of ANSI-C Programs Using SAT
door: Clarke, E, et al.
Gepubliceerd in: (2004)

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

Functions with local state: regularity and undecidability
door: Murawski, A
Gepubliceerd in: (2005)

An algebraic theory of componentised interaction
door: Chilton, C
Gepubliceerd in: (2013)

On learning assumptions for compositional verification of probabilistic systems
door: Feng, L
Gepubliceerd in: (2014)

Program analysis with interpolants
door: Weissenbacher, G, et al.
Gepubliceerd in: (2010)

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

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

Techniques and tools for the verification of concurrent systems
door: Palikareva, H
Gepubliceerd in: (2012)

Repairing strings and trees
door: Riveros Jaeger, C
Gepubliceerd in: (2013)

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

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

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

Abstract satisfaction
door: Haller, L
Gepubliceerd in: (2013)

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

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

Higher-order semantics for quantum programming languages with classical control
door: Atzemoglou, GP
Gepubliceerd in: (2012)

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

Verificator: Educational Tool for Learning Programming
door: Danijel RADOSEVIC, et al.
Gepubliceerd in: (2009-10-01)

Program synthesis from domain specific object models
door: Faitelson, D
Gepubliceerd in: (2008)

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

Testimony on Voter Verification
door: Selker, Ted
Gepubliceerd in: (2015)

EL-ifying ontologies
door: Carral, D, et al.
Gepubliceerd in: (2014)

Static analyses over weak memory
door: Nimal, V, et al.
Gepubliceerd in: (2014)

Pushing the boundaries of tractable ontology reasoning
door: Carral, D, et al.
Gepubliceerd in: (2014)

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

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

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