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

Disgrifiad llawn

Manylion Llyfryddiaeth
Prif Awdur:	Lewis, M
Awduron Eraill:	Kroening, D
Fformat:	Traethawd Ymchwil
Iaith:	English
Cyhoeddwyd:	2014
Pynciau:	Theory and automated verification

Eitemau Tebyg

Automated quantitative software verification
gan: Kattenbelt, M
Cyhoeddwyd: (2010)

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

Monotonicity in shared-memory program verification
gan: Kaiser, A
Cyhoeddwyd: (2013)

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

Forward looking logics and automata
gan: Ley, C
Cyhoeddwyd: (2011)

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

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

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

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

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

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

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

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

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

Functions with local state: regularity and undecidability
gan: Murawski, A
Cyhoeddwyd: (2005)

An algebraic theory of componentised interaction
gan: Chilton, C
Cyhoeddwyd: (2013)

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

Program analysis with interpolants
gan: Weissenbacher, G, et al.
Cyhoeddwyd: (2010)

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

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

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

Repairing strings and trees
gan: Riveros Jaeger, C
Cyhoeddwyd: (2013)

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

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

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

Abstract satisfaction
gan: Haller, L
Cyhoeddwyd: (2013)

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

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

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

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

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

Program synthesis from domain specific object models
gan: Faitelson, D
Cyhoeddwyd: (2008)

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

Testimony on Voter Verification
gan: Selker, Ted
Cyhoeddwyd: (2015)

EL-ifying ontologies
gan: Carral, D, et al.
Cyhoeddwyd: (2014)

Static analyses over weak memory
gan: Nimal, V, et al.
Cyhoeddwyd: (2014)

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

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

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

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