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