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

Cur síos iomlán

Sonraí bibleagrafaíochta
Príomhchruthaitheoir:	Lewis, M
Rannpháirtithe:	Kroening, D
Formáid:	Tráchtas
Teanga:	English
Foilsithe / Cruthaithe:	2014
Ábhair:	Theory and automated verification

Míreanna comhchosúla

Automated quantitative software verification
de réir: Kattenbelt, M
Foilsithe / Cruthaithe: (2010)

Quantitative verification of real-time properties with application to medical devices
de réir: Marco Diciolla, M, et al.
Foilsithe / Cruthaithe: (2014)

Monotonicity in shared-memory program verification
de réir: Kaiser, A
Foilsithe / Cruthaithe: (2013)

Intersection types and higer-order model checking
de réir: Ramsay, S, et al.
Foilsithe / Cruthaithe: (2014)

Forward looking logics and automata
de réir: Ley, C
Foilsithe / Cruthaithe: (2011)

Probabilistic guarded commands mechanized in HOL
de réir: Hurd, J, et al.
Foilsithe / Cruthaithe: (2005)

Incremental modelling for verified communication architectures
de réir: Boehm, P, et al.
Foilsithe / Cruthaithe: (2011)

Game semantics based equivalence checking of higher-order programs
de réir: Hopkins, D, et al.
Foilsithe / Cruthaithe: (2012)

Partial correctness for probabilistic demonic programs
de réir: McIver, A, et al.
Foilsithe / Cruthaithe: (2001)

Automated Verification of Building Components Using BIM Models and Point Clouds
de réir: Honti Richard, et al.
Foilsithe / Cruthaithe: (2020-09-01)

Verification of asynchronous concurrency and the shaped stack constraint
de réir: Kochems, J
Foilsithe / Cruthaithe: (2014)

Abstraction discovery and refinement for model checking by symbolic trajectory evaluation
de réir: Adams, S
Foilsithe / Cruthaithe: (2014)

Predicate Abstraction of ANSI-C Programs Using SAT
de réir: Clarke, E, et al.
Foilsithe / Cruthaithe: (2004)

Automation Processes for Efficient Verification of Complex Systems: An Empirical Case Study
de réir: Rune Andre Haugen, et al.
Foilsithe / Cruthaithe: (2024-12-01)

Functions with local state: regularity and undecidability
de réir: Murawski, A
Foilsithe / Cruthaithe: (2005)

An algebraic theory of componentised interaction
de réir: Chilton, C
Foilsithe / Cruthaithe: (2013)

On learning assumptions for compositional verification of probabilistic systems
de réir: Feng, L
Foilsithe / Cruthaithe: (2014)

Program analysis with interpolants
de réir: Weissenbacher, G, et al.
Foilsithe / Cruthaithe: (2010)

C Program Verification: VC Explanation and the Standard Library
de réir: A. V. Promsky
Foilsithe / Cruthaithe: (2011-12-01)

Criticality Analysis for the Verification and Validation of Automated Vehicles
de réir: Christian Neurohr, et al.
Foilsithe / Cruthaithe: (2021-01-01)

Techniques and tools for the verification of concurrent systems
de réir: Palikareva, H
Foilsithe / Cruthaithe: (2012)

Repairing strings and trees
de réir: Riveros Jaeger, C
Foilsithe / Cruthaithe: (2013)

An interpolating decision procedure for transitive relations with uninterpreted functions
de réir: Kroening, D, et al.
Foilsithe / Cruthaithe: (2009)

Verification of the expert’s opinion
de réir: M. H. Shcherbakovskyi, et al.
Foilsithe / Cruthaithe: (2022-09-01)

A New Method for Verification and Evaluation of PLC Software
de réir: Muhammed Ali Nur ÖZ, et al.
Foilsithe / Cruthaithe: (2023-06-01)

Abstract satisfaction
de réir: Haller, L
Foilsithe / Cruthaithe: (2013)

Coverage Fulfillment Automation in Hardware Functional Verification Using Genetic Algorithms
de réir: Gabriel Mihail Danciu, et al.
Foilsithe / Cruthaithe: (2022-01-01)

On Construction and Verification of PLC-Programs
de réir: E. V. Kuzmin, et al.
Foilsithe / Cruthaithe: (2015-02-01)

Higher-order semantics for quantum programming languages with classical control
de réir: Atzemoglou, GP
Foilsithe / Cruthaithe: (2012)

Explainability of Automated Fact Verification Systems: A Comprehensive Review
de réir: Manju Vallayil, et al.
Foilsithe / Cruthaithe: (2023-11-01)

Verificator: Educational Tool for Learning Programming
de réir: Danijel RADOSEVIC, et al.
Foilsithe / Cruthaithe: (2009-10-01)

Program synthesis from domain specific object models
de réir: Faitelson, D
Foilsithe / Cruthaithe: (2008)

Wall Structure Geometry Verification Using TLS Data and BIM Model
de réir: Gabriela Bariczová, et al.
Foilsithe / Cruthaithe: (2021-12-01)

Testimony on Voter Verification
de réir: Selker, Ted
Foilsithe / Cruthaithe: (2015)

EL-ifying ontologies
de réir: Carral, D, et al.
Foilsithe / Cruthaithe: (2014)

Static analyses over weak memory
de réir: Nimal, V, et al.
Foilsithe / Cruthaithe: (2014)

Pushing the boundaries of tractable ontology reasoning
de réir: Carral, D, et al.
Foilsithe / Cruthaithe: (2014)

Reinforcement Learning Made Affordable for Hardware Verification Engineers
de réir: Alexandru Dinu, et al.
Foilsithe / Cruthaithe: (2022-11-01)

Tractable query answering for description logics via query rewriting
de réir: Perez-Urbina, H, et al.
Foilsithe / Cruthaithe: (2010)

Automation of Formal Veriﬁcation of Programs in the Pifagor Language
de réir: M. S. Ushakova, et al.
Foilsithe / Cruthaithe: (2015-08-01)