Salvatore LA TORRE | Automatic Techniquesfor Software Verification
Salvatore LA TORRE Automatic Techniquesfor Software Verification
cod. 0522500076
AUTOMATIC TECHNIQUESFOR SOFTWARE VERIFICATION
| 0522500076 | |
| DIPARTIMENTO DI INFORMATICA | |
| EQF7 | |
| COMPUTER SCIENCE | |
| 2016/2017 |
| YEAR OF COURSE 2 | |
| YEAR OF DIDACTIC SYSTEM 2015 | |
| PRIMO SEMESTRE |
| SSD | CFU | HOURS | ACTIVITY | |
|---|---|---|---|---|
| INF/01 | 6 | 48 | LESSONS |
| Objectives | |
|---|---|
| -KNOWLEDGE AND UNDERSTANDING: ACQUISITION OF THE BASIC UNDERSTANDING OF THE MAIN TECHNIQUES USED IN THE AUTOMATIC VERIFICATION OF PROGRAMS BASED ON THE MODEL-CHECKING AND TESTING. UNDERSTANDING OF THE DIFFERENCES AND THE COMPLEMENTARITY WITH THE OTHER TECHNIQUES THAT ARE USED FOR VERIFICATION IN PRACTICE. UNDERSTANDING OF THE MAIN PROBLEMS OF USING THESE TECHNOLOGIES. LEARNING OF THE MAIN ALGORITHMS. -APPLYING KNOWLEDGE AND UNDERSTANDING: ABILITY TO IDENTIFY THE CLASS OF MODELS AND SPECIFICATION LANGUAGES WHICH ARE THE MOST SUITABLE FOR THE PROGRAMS TO ANALYZE. ABILITY TO USE A MODEL-CHECKER FOR VERIFYING CORRECTNESS OF REAL SYSTEMS. CAPACITY TO TUNE THE TOOLS TO PERFORM THE ANALYSIS OF VERY COMPLEX PROGRAMS. -MAKING JUDGEMENTS: DISCUSSION OF THE PROS AND CONS OF THE STUDIED TECHNIQUES AND SOLUTIONS. ANALYSIS OF THE DEVELOPPED PROJECTS. INDIVIDUAL SEARCH OF THE MATERIAL FOR A DEEPER UNDERSTANDING OF SELECTED TOPICS. -COMMUNICATION SKILLS: PARTICIPATION TO THE DESIGN A SOLUTION FOR THE PROPOSED PROBLEMS. PRESENTATION AND DISCUSSION OF THE DETERMINED SOLUTIONS. ACTIVE PARTICIPATION TO THE LECTURES AND THE SEMINARS. -LEARNING SKILLS: INDIVIDUAL STUDY OF SELECTED TOPICS. SEARCH OF NEW TOOLS FOR INTERESTING CLASES OF PROGRAMS. |
| Prerequisites | |
|---|---|
| BASIC UNDERSTANDING OF FINITE AUTOMATA, PUSHDOWN AUTOMATA, PROCEDURAL PROGRAMMING, BOOLEAN LOGIC AND COMPUTATIONAL COMPLEXITY. |
| Contents | |
|---|---|
| INTRODUCTION. CORRECTNESS OF PROGRAMS. SPECIFICATION. NOTION OF ERROR. TOOLS FOR VERIFYING PROGRAM CORRECTNESS. PART A: FOUNDATIONS OF SOFTWARE TESTING: - ANALYSIS OF SPECIFICATION - TESTING AND SIMULATION - BLACK-BOX/WHITE-BOX TESTING (STATIC AND DYNAMIC) - UNIT AND INTEGRATION TESTING - DATA/CODE COVERAGE - TEST TOOLS - TESTING AUTOMATION - RANDOM TESTING - TEST SHARING - BETA TESTING - MODEL-BASED TESTING PART B: MODEL-CHECKING - THE MODEL-CHECKING TECHNOLOGY. BASIC CONCEPTS. - FOUNDATIONS: AUTOMATA, TEMPORAL LOGIC, COMPUTATIONAL COMPLEXITY. - EXPLICIT MODEL-CHECKING - SYMBOLIC MODEL-CHECKING - BOUNDED MODEL-CHECKING - MODEL-CHECKING USING PUSHDOWN AUTOMATA - MODEL-CHECKING REAL CODE - ABSTRACTIONS - COUNTER-EXAMPLE GUIDED ABSTRACTION REFINEMENT (CEGAR LOOP) - IMPLEMENTING MODEL-CHECKERS WITH FIXED-POINT LOGIC - CONCURRENT SOFTWARE - BOUNDED-CONTEXT SWITCHING - SEQUENTIALIZATION - MODEL-BASED TESTING USING MODEL-CHECKERS |
| Teaching Methods | |
|---|---|
| THE LECTURES ON THE THEORETICAL ASPECTS OF THE COURSE TOPICS ARE HELD IN A STANDARD CLASSROOM, BY USING POWERPOINT PRESENTATIONS OR SIMILAR. ON EACH TOPIC, THE STUDENTS ARE INVOLVED IN AN ACCURATE DISCUSSION AND, WHERE APPROPRIATE, COMPARISONS WITH ALTERNATIVE SOLUTIONS ARE DONE. THE LECTURES ON THE PRACTICAL ASPECTS CONSISTS OF PERFORMING EXPERIMENTS ON PC. IN PARTICULAR, MODELS OF PROGRAMS ARE IMPLEMENTED, OR PROGRAMS OR MODELS ARE TAKEN FROM THE AVAILABLE BENCHMARKS FOR THE VARIOUS TOOLS, AND SESSIONS OF PROGRAM VERIFICATION AND ANALYSIS OF THE OBTAINED RESULTS ARE PERFORMED. THE EXPERIMENTS ARE CONDUCTED INDIVIDUALLY BY EACH STUDENT, AND ARE FOLLOWED BY A DISCUSSION IN WHICH THE INDIVIDUAL EXPERIENCES ARE COMPARED. |
| Verification of learning | |
|---|---|
| INDIVIDUAL PROJECT ON ISSUES PERTAINING TO THE COURSE PROGRAM. PRESENTATION OF THE PROJECT TO THE REST OF THE CLASS FOLLOWED BY A DISCUSSION ON THE DESCRIBED CONCEPTS AND METHODS. INTERVIEW OVER THE TOPICS OF THE COURSE PROGRAM. THE ABILITY OF CARRYING ON THE PROJECT AUTONOMOUSLY, THE ABILITY OF SELECTING THE MAIN ASPECTS OF THE PROPOSED TOPICS, A DEEP UNDERSTANDING OF THE TECHNICAL DETAILS AND OF THE PRACTICAL CONSEQUENCES, AND THE CLARITY OF PRESENTATION ARE POSITIVELY EVALUATED. |
| Texts | |
|---|---|
| -MORDECHAI BEN-ARI PRICIPLES OF THE SPIN MODEL CHECKER SPRINGER, ISBN 978-1-84628-769-5. -GERARD J. HOLZMANN THE SPIN MODEL CHECKER: PRIMER AND REFERENCE MANUAL ADDISON WESLEY, ISBN 0-321-22862-6. CLASS NOTES AND SCIENTIFIC PAPERS THEREIN CITED. |
BETA VERSION Data source ESSE3 [Ultima Sincronizzazione: 2019-03-11]
