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)