Comparing Verification Condition Generation with Symbolic Execution: An Experience Report (Englisch)
- Neue Suche nach: Kassios, Ioannis T.
- Neue Suche nach: Müller, Peter
- Neue Suche nach: Schwerhoff, Malte
- Neue Suche nach: Kassios, Ioannis T.
- Neue Suche nach: Müller, Peter
- Neue Suche nach: Schwerhoff, Malte
In:
Verified Software: Theories, Tools, Experiments
;
196-208
;
2012
- Aufsatz/Kapitel (Buch) / Elektronische Ressource
-
Titel:Comparing Verification Condition Generation with Symbolic Execution: An Experience Report
-
Beteiligte:
-
Erschienen in:Lecture Notes in Computer Science ; 7152 ; 196-208
-
Verlag:
- Neue Suche nach: Springer Berlin Heidelberg
-
Erscheinungsort:Berlin, Heidelberg
-
Erscheinungsdatum:01.01.2012
-
Format / Umfang:13 pages
-
ISBN:
-
ISSN:
-
DOI:
-
Medientyp:Aufsatz/Kapitel (Buch)
-
Format:Elektronische Ressource
-
Sprache:Englisch
-
Schlagwörter:
-
Datenquelle:
Inhaltsverzeichnis E-Book
Die Inhaltsverzeichnisse werden automatisch erzeugt und basieren auf den im Index des TIB-Portals verfügbaren Einzelnachweisen der enthaltenen Beiträge. Die Anzeige der Inhaltsverzeichnisse kann daher unvollständig oder lückenhaft sein.
- 1
-
Cyber War, Formal Verification and Certified InfrastructurePaul, Wolfgang et al. | 2012
- 2
-
A Certified Multi-prover Verification Condition GeneratorHerms, Paolo / Marché, Claude / Monate, Benjamin et al. | 2012
- 18
-
Integrated Semantics of Intermediate-Language C and Macro-Assembler for Pervasive Formal Verification of Operating Systems and Hypervisors from VerisoftXTSchmaltz, Sabine / Shadrin, Andrey et al. | 2012
- 34
-
The Location Linking Concept: A Basis for Verification of Code Using PointersKulczycki, Gregory / Smith, Hampton / Harton, Heather / Sitaraman, Murali / Ogden, William F. / Hollingsworth, Joseph E. et al. | 2012
- 50
-
Verifying Implementations of Security Protocols by RefinementPolikarpova, Nadia / Moskal, Michał et al. | 2012
- 66
-
Deciding Functional Lists with Sublist SetsWies, Thomas / Muñiz, Marco / Kuncak, Viktor et al. | 2012
- 82
-
Developing Verified Programs with DafnyRustan, K. / Leino, M. et al. | 2012
- 83
-
Verifying Two Lines of C with Why3: An Exercise in Program VerificationFilliâtre, Jean-Christophe et al. | 2012
- 98
-
Development and Evaluation of LAV: An SMT-Based Error Finding PlatformVujošević-Janičić, Milena / Kuncak, Viktor et al. | 2012
- 114
-
A Lightweight Technique for Distributed and Incremental Program VerificationBrain, Martin / Schanda, Florian et al. | 2012
- 130
-
A Comparison of Intermediate Verification Languages: Boogie and Sireum/PilarSegal, Loren / Chalin, Patrice et al. | 2012
- 146
-
LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IRMerz, Florian / Falke, Stephan / Sinz, Carsten et al. | 2012
- 162
-
The Marriage of Exploration and DeductionMajumdar, Rupak et al. | 2012
- 163
-
Modeling and Validating the Train Fare Calculation and Adjustment System Using VDM++Tang, Nguyen / Souma, Daisuke / Hatayama, Goro / Ohsaki, Hitoshi et al. | 2012
- 179
-
Formalized Verification of Snapshotable Trees: Separation and SharingMehnert, Hannes / Sieczkowski, Filip / Birkedal, Lars / Sestoft, Peter et al. | 2012
- 196
-
Comparing Verification Condition Generation with Symbolic Execution: An Experience ReportKassios, Ioannis T. / Müller, Peter / Schwerhoff, Malte et al. | 2012
- 209
-
Verification of TLB Virtualization Implemented in CAlkassar, Eyad / Cohen, Ernie / Kovalev, Mikhail / Paul, Wolfgang J. et al. | 2012
- 225
-
Formalization and Analysis of Real-Time Requirements: A Feasibility Study at BOSCHPost, Amalinda / Hoenicke, Jochen et al. | 2012
- 241
-
Our Experience with the CodeContracts Static CheckerLogozzo, Francesco et al. | 2012
- 243
-
Isabelle/Circus: A Process Specification and Verification EnvironmentFeliachi, Abderrahmane / Gaudel, Marie-Claude / Wolff, Burkhart et al. | 2012
- 261
-
Termination Analysis of Imperative Programs Using Bitvector ArithmeticFalke, Stephan / Kapur, Deepak / Sinz, Carsten et al. | 2012
- 278
-
Specifying and Verifying the Correctness of Dynamic Software UpdatesHayden, Christopher M. / Magill, Stephen / Hicks, Michael / Foster, Nate / Foster, Jeffrey S. et al. | 2012
- 294
-
Symbolic Execution Enhanced System TestingDavies, Misty / Păsăreanu, Corina S. / Raman, Vishwanath et al. | 2012
- 310
-
Infeasible Code DetectionBertolini, Cristiano / Schäf, Martin / Schweitzer, Pascal et al. | 2012