Salvatore LA TORRE | AUTOMATIC TECHNIQUESFOR SOFTWARE VERIFICATION
Salvatore LA TORRE AUTOMATIC TECHNIQUESFOR SOFTWARE VERIFICATION
cod. 0522500076
AUTOMATIC TECHNIQUESFOR SOFTWARE VERIFICATION
| 0522500076 | |
| COMPUTER SCIENCE | |
| EQF7 | |
| COMPUTER SCIENCE | |
| 2024/2025 |
| YEAR OF DIDACTIC SYSTEM 2016 | |
| AUTUMN SEMESTER |
| 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. |
| 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, BASIC NOTIONS OF TESTING (4 HRS) THE MODEL-CHECKING TECHNOLOGY, BASIC CONCEPTS (2 HRS) FOUNDATIONS: AUTOMATA, TEMPORAL LOGIC, COMPUTATIONAL COMPLEXITY (8 HRS) EXPLICIT MODEL-CHECKING (4 HRS) SYMBOLIC MODEL-CHECKING (4 HRS) BOUNDED MODEL-CHECKING (4 HRS) MODEL-CHECKING USING PUSHDOWN AUTOMATA (4 HRS) MODEL-CHECKING REAL CODE, ABSTRACTIONS COUNTER-EXAMPLE GUIDED ABSTRACTION REFINEMENT: CEGAR LOOP (4 HRS) IMPLEMENTING MODEL-CHECKERS WITH FIXED-POINT LOGIC (4 HRS) CONCURRENT SOFTWARE, BOUNDED-CONTEXT SWITCHING, SEQUENTIALIZATION (8 HRS) MODEL-BASED TESTING USING MODEL-CHECKERS (2 HRS) |
| 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 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. THE EXAM WILL BE GRADED WITH A SCORE UP TO 30 BY TAKING INTO ACCOUNT ALL THE ABOVE ASPECTS. |
| 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 |
| More Information | |
|---|---|
| ATTENDANCE AT THE LECTURES IS STRONGLY RECOMMENDED. |
BETA VERSION Data source ESSE3 [Ultima Sincronizzazione: 2024-11-18]
