Program Semantics, Specification and Verification: Theory and Applications (190,00 руб.)

8th International Computer Science Symposium in Russia Fourth Workshop Program Semantics, Specication and Verication: Theory and Applications Yekaterinburg, Russia, June 24, 2013 Proceedings Valery Nepomniaschy, Valery Sokolov (Eds.) Yaroslavl 2013 ÓÄÊ 519.68 ÁÁÊ Â185.2ÿ43 Ñ30 Program Semantics, Specication Applications. <...> Proceedings of the IV and Verication: International Theory Workshop PSSV and 2013. <...> Workshop on Program Semantics, Specication and Verication: Theory and Applications is the leading event in Russia in the eld of applying of the formal methods to software analysis. <...> Proceedings of the fourth workshop dedicated to formalisms for program semantics, formal models and verication, programming and specication languages, etc. <...> ISBN 9785839709355 c Yaroslavl State University, 2013 Preface The volume contains the papers selected for presentation at the Fourth International Workshop on Program Semantics, Specication and Verication: Theory and Applications (PSSV 2013) aliated with the 8th International Symposium Computer Science in Russia (CSR 2013). <...> The topics of the Workshop include formal models of programs and systems, methods of formal semantics of programming languages, formal specication languages, methods of deductive program verication, model checking method, static analysis of programs, formal approaches to testing and validation, program testing, analysis and verication tools. 11 papers have been submitted to PSSV 2013. <...> We are grateful to Irina Adrianova and Alexei Promsky for considerable eorts in preparing the proceedings. <...> It is based on combining several recent results in BMC, namely: use of LLVM as a baseline for model generation, employment of high-performance Z3 SMT solver to do the formula heavy-lifting, and use of various function summaries to improve analysis eciency and expressive power. <...> Bounded Model Checking, Satisability Modulo Theories, LLVM, Function Contracts, Function Summaries Keywords: 1 Introduction Nowadays, dierent kinds of software are widely used almost everywhere, from nuclear power plants and aircrafts to smart homes and kitchen appliances. <...> Generation of software model for BMC We use an approach very similar to LLBMC [21] and extract a model from an internal LLVM compiler representation (LLVM IR) instead of a C/C++ source code itself. <...> This allows us to work with a much <...>