000 | 03855nam a22005415i 4500 | ||
---|---|---|---|
001 | 978-3-031-02551-8 | ||
003 | DE-He213 | ||
005 | 20240730164000.0 | ||
007 | cr nn 008mamaa | ||
008 | 220601s2020 sz | s |||| 0|eng d | ||
020 |
_a9783031025518 _9978-3-031-02551-8 |
||
024 | 7 |
_a10.1007/978-3-031-02551-8 _2doi |
|
050 | 4 | _aT1-995 | |
072 | 7 |
_aTBC _2bicssc |
|
072 | 7 |
_aTEC000000 _2bisacsh |
|
072 | 7 |
_aTBC _2thema |
|
082 | 0 | 4 |
_a620 _223 |
100 | 1 |
_aPăsăreanu, Corina S. _eauthor. _4aut _4http://id.loc.gov/vocabulary/relators/aut _981482 |
|
245 | 1 | 0 |
_aSymbolic Execution and Quantitative Reasoning _h[electronic resource] : _bApplications to Software Safety and Security / _cby Corina S. Păsăreanu. |
250 | _a1st ed. 2020. | ||
264 | 1 |
_aCham : _bSpringer International Publishing : _bImprint: Springer, _c2020. |
|
300 |
_aIX, 65 p. _bonline resource. |
||
336 |
_atext _btxt _2rdacontent |
||
337 |
_acomputer _bc _2rdamedia |
||
338 |
_aonline resource _bcr _2rdacarrier |
||
347 |
_atext file _bPDF _2rda |
||
490 | 1 |
_aSynthesis Lectures on Software Engineering, _x2328-3327 |
|
505 | 0 | _aAcknowledgments -- Introduction -- Symbolic Execution: The Basics -- Symbolic Complexity Analysis -- Probabilistic Reasoning -- Side-Channel Analysis -- Conclusion and Directions for the Future -- Bibliography -- Author's Biography. | |
520 | _aThis book reviews recent advances in symbolic execution and its probabilistic variant and discusses how they can be used to ensure the safety and security of software systems. Symbolic execution is a systematic program analysis technique which explores multiple program behaviors all at once by collecting and solving symbolic constraints collected from the branching conditions in the program. The obtained solutions can be used as test inputs that execute feasible program paths. Symbolic execution has found many applications in various domains, such as security, smartphone applications, operating systems, databases, and more recently deep neural networks, uncovering subtle errors and unknown vulnerabilities. We review here the technique has also been extended to reason about algorithmic complexity and resource consumption. Furthermore, symbolic execution has been recently extended with probabilistic reasoning, allowing one to reason about quantitative properties of software systems. The approach computes the conditions to reach target program events of interest and uses model counting to quantify the fraction of the input domain satisfying these conditions thus computing the probability of event occurrence. This probabilistic information can be used for example to compute the reliability of an aircraft controller under different wind conditions (modeled probabilistically) or to quantify the leakage of sensitive data in a software system, using information theory metrics such as Shannon entropy. This book is intended for students and software engineers who are interested in advanced techniques for testing and verifying software systems. | ||
650 | 0 |
_aEngineering. _99405 |
|
650 | 0 |
_aMathematics. _911584 |
|
650 | 0 |
_aComputer science. _99832 |
|
650 | 0 |
_aSoftware engineering. _94138 |
|
650 | 1 | 4 |
_aTechnology and Engineering. _981483 |
650 | 2 | 4 |
_aMathematics. _911584 |
650 | 2 | 4 |
_aComputer Science. _99832 |
650 | 2 | 4 |
_aSoftware Engineering. _94138 |
710 | 2 |
_aSpringerLink (Online service) _981484 |
|
773 | 0 | _tSpringer Nature eBook | |
776 | 0 | 8 |
_iPrinted edition: _z9783031003417 |
776 | 0 | 8 |
_iPrinted edition: _z9783031014239 |
776 | 0 | 8 |
_iPrinted edition: _z9783031036798 |
830 | 0 |
_aSynthesis Lectures on Software Engineering, _x2328-3327 _981485 |
|
856 | 4 | 0 | _uhttps://doi.org/10.1007/978-3-031-02551-8 |
912 | _aZDB-2-SXSC | ||
942 | _cEBK | ||
999 |
_c85183 _d85183 |