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

Полное описание

Библиографические подробности
Главный автор:	Lewis, M
Другие авторы:	Kroening, D
Формат:	Диссертация
Язык:	English
Опубликовано:	2014
Предметы:	Theory and automated verification

Схожие документы

Automated quantitative software verification
по: Kattenbelt, M
Опубликовано: (2010)

Quantitative verification of real-time properties with application to medical devices
по: Marco Diciolla, M, и др.
Опубликовано: (2014)

Monotonicity in shared-memory program verification
по: Kaiser, A
Опубликовано: (2013)

Intersection types and higer-order model checking
по: Ramsay, S, и др.
Опубликовано: (2014)

Forward looking logics and automata
по: Ley, C
Опубликовано: (2011)

Probabilistic guarded commands mechanized in HOL
по: Hurd, J, и др.
Опубликовано: (2005)

Incremental modelling for verified communication architectures
по: Boehm, P, и др.
Опубликовано: (2011)

Game semantics based equivalence checking of higher-order programs
по: Hopkins, D, и др.
Опубликовано: (2012)

Partial correctness for probabilistic demonic programs
по: McIver, A, и др.
Опубликовано: (2001)

Automated Verification of Building Components Using BIM Models and Point Clouds
по: Honti Richard, и др.
Опубликовано: (2020-09-01)

Verification of asynchronous concurrency and the shaped stack constraint
по: Kochems, J
Опубликовано: (2014)

Abstraction discovery and refinement for model checking by symbolic trajectory evaluation
по: Adams, S
Опубликовано: (2014)

Predicate Abstraction of ANSI-C Programs Using SAT
по: Clarke, E, и др.
Опубликовано: (2004)

Automation Processes for Efficient Verification of Complex Systems: An Empirical Case Study
по: Rune Andre Haugen, и др.
Опубликовано: (2024-12-01)

Functions with local state: regularity and undecidability
по: Murawski, A
Опубликовано: (2005)

An algebraic theory of componentised interaction
по: Chilton, C
Опубликовано: (2013)

On learning assumptions for compositional verification of probabilistic systems
по: Feng, L
Опубликовано: (2014)

Program analysis with interpolants
по: Weissenbacher, G, и др.
Опубликовано: (2010)

C Program Verification: VC Explanation and the Standard Library
по: A. V. Promsky
Опубликовано: (2011-12-01)

Criticality Analysis for the Verification and Validation of Automated Vehicles
по: Christian Neurohr, и др.
Опубликовано: (2021-01-01)

Techniques and tools for the verification of concurrent systems
по: Palikareva, H
Опубликовано: (2012)

Repairing strings and trees
по: Riveros Jaeger, C
Опубликовано: (2013)

An interpolating decision procedure for transitive relations with uninterpreted functions
по: Kroening, D, и др.
Опубликовано: (2009)

Verification of the expert’s opinion
по: M. H. Shcherbakovskyi, и др.
Опубликовано: (2022-09-01)

A New Method for Verification and Evaluation of PLC Software
по: Muhammed Ali Nur ÖZ, и др.
Опубликовано: (2023-06-01)

Abstract satisfaction
по: Haller, L
Опубликовано: (2013)

Coverage Fulfillment Automation in Hardware Functional Verification Using Genetic Algorithms
по: Gabriel Mihail Danciu, и др.
Опубликовано: (2022-01-01)

On Construction and Verification of PLC-Programs
по: E. V. Kuzmin, и др.
Опубликовано: (2015-02-01)

Higher-order semantics for quantum programming languages with classical control
по: Atzemoglou, GP
Опубликовано: (2012)

Explainability of Automated Fact Verification Systems: A Comprehensive Review
по: Manju Vallayil, и др.
Опубликовано: (2023-11-01)

Verificator: Educational Tool for Learning Programming
по: Danijel RADOSEVIC, и др.
Опубликовано: (2009-10-01)

Program synthesis from domain specific object models
по: Faitelson, D
Опубликовано: (2008)

Wall Structure Geometry Verification Using TLS Data and BIM Model
по: Gabriela Bariczová, и др.
Опубликовано: (2021-12-01)

Testimony on Voter Verification
по: Selker, Ted
Опубликовано: (2015)

EL-ifying ontologies
по: Carral, D, и др.
Опубликовано: (2014)

Static analyses over weak memory
по: Nimal, V, и др.
Опубликовано: (2014)

Pushing the boundaries of tractable ontology reasoning
по: Carral, D, и др.
Опубликовано: (2014)

Reinforcement Learning Made Affordable for Hardware Verification Engineers
по: Alexandru Dinu, и др.
Опубликовано: (2022-11-01)

Tractable query answering for description logics via query rewriting
по: Perez-Urbina, H, и др.
Опубликовано: (2010)

Automation of Formal Veriﬁcation of Programs in the Pifagor Language
по: M. S. Ushakova, и др.
Опубликовано: (2015-08-01)