A Late Treatment of C Precondition in Dynamic Symbolic Execution
| Autor: | Mickaël Delahaye, Nikolai Kosmatov |
|---|---|
| Přispěvatelé: | Validation de Systèmes, Composants et Objets logiciels (VASCO), Laboratoire d'Informatique de Grenoble (LIG), Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF), Laboratoire Sûreté des Logiciels (LSL), Département Ingénierie Logiciels et Systèmes (DILS), Laboratoire d'Intégration des Systèmes et des Technologies (LIST), Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay-Laboratoire d'Intégration des Systèmes et des Technologies (LIST), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay, French-government Single Inter-Ministry Fund (FUI) through the IO32 project (Instrumentation and Tools for 32-bit Microcontrollers), Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay-Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA)) |
| Jazyk: | angličtina |
| Rok vydání: | 2013 |
| Předmět: |
dynamic symbolic execution
Programming language Computer science 020207 software engineering Context (language use) 02 engineering and technology executable preconditions [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] computer.software_genre Symbolic execution Rotation formalisms in three dimensions Electronic mail Precondition test input generation Test case Test Context 0202 electrical engineering electronic engineering information engineering Concolic testing 020201 artificial intelligence & image processing computer concolic testing |
| Zdroj: | CSTVA 2013-5th International Workshop on Constraints in Software Testing, Verification, and Analysis CSTVA 2013-5th International Workshop on Constraints in Software Testing, Verification, and Analysis, Aug 2013, Luxembourg, Luxembourg. pp.230-231, ⟨10.1109/ICSTW.2013.34⟩ ICST Workshops |
| DOI: | 10.1109/ICSTW.2013.34⟩ |
| Popis: | CSTVA Session 2; International audience; Relevance of automatically generated test cases depends on an appropriate definition of a test context, or precondition. This paper presents a novel method for handling a precondition in dynamic symbolic execution (DSE) testing tools. This method allows Path Crawler, a DSE tool for C~programs, to accept a precondition defined as a C function. It provides a simple way to express a precondition even for developers who are not familiar with specification formalisms. It has also proven useful when combining static and dynamic analysis. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|