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

Descrizione completa

Dettagli Bibliografici
Autore principale:	Lewis, M
Altri autori:	Kroening, D
Natura:	Tesi
Lingua:	English
Pubblicazione:	2014
Soggetti:	Theory and automated verification

Documenti analoghi

Automated quantitative software verification
di: Kattenbelt, M
Pubblicazione: (2010)

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

Monotonicity in shared-memory program verification
di: Kaiser, A
Pubblicazione: (2013)

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

Forward looking logics and automata
di: Ley, C
Pubblicazione: (2011)

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

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

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

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

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

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

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

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

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

Functions with local state: regularity and undecidability
di: Murawski, A
Pubblicazione: (2005)

An algebraic theory of componentised interaction
di: Chilton, C
Pubblicazione: (2013)

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

Program analysis with interpolants
di: Weissenbacher, G, et al.
Pubblicazione: (2010)

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

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

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

Repairing strings and trees
di: Riveros Jaeger, C
Pubblicazione: (2013)

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

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

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

Abstract satisfaction
di: Haller, L
Pubblicazione: (2013)

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

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

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

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

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

Program synthesis from domain specific object models
di: Faitelson, D
Pubblicazione: (2008)

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

Testimony on Voter Verification
di: Selker, Ted
Pubblicazione: (2015)

EL-ifying ontologies
di: Carral, D, et al.
Pubblicazione: (2014)

Static analyses over weak memory
di: Nimal, V, et al.
Pubblicazione: (2014)

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

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

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

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