LEADER 03093nam 22006132 450 001 9910452089903321 005 20151005020622.0 010 $a1-107-18286-7 010 $a1-281-08499-9 010 $a9786611084998 010 $a0-511-34188-1 010 $a0-511-34134-2 010 $a0-511-34076-1 010 $a0-511-57396-0 010 $a0-511-61909-X 010 $a0-511-34241-1 035 $a(CKB)1000000000478585 035 $a(EBL)326024 035 $a(OCoLC)667096303 035 $a(SSID)ssj0000203083 035 $a(PQKBManifestationID)11166861 035 $a(PQKBTitleCode)TC0000203083 035 $a(PQKBWorkID)10258525 035 $a(PQKB)11281418 035 $a(UkCbUP)CR9780511619090 035 $a(MiAaPQ)EBC326024 035 $a(Au-PeEL)EBL326024 035 $a(CaPaEBR)ebr10196250 035 $a(CaONFJC)MIL108499 035 $a(EXLCZ)991000000000478585 100 $a20090915d2007|||| uy| 0 101 0 $aeng 135 $aur||||||||||| 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 14$aThe Milos?evic? trial $elessons for the conduct of complex international criminal proceedings /$fGideon Boas$b[electronic resource] 210 1$aCambridge :$cCambridge University Press,$d2007. 215 $a1 online resource (xviii, 306 pages) $cdigital, PDF file(s) 300 $aTitle from publisher's bibliographic system (viewed on 05 Oct 2015). 311 $a0-521-70039-6 311 $a0-521-87699-0 327 $aFair and Expeditious International Criminal Trials -- The Milos?evic? Prosecution Case -- Getting Off on the Wrong Foot -- Case Management Challenges in the Milos?evic? Trial -- Representation and Resource Issues in International Criminal Law -- Conclusions. 330 $aWhen Slobodan Milos?evic? died in the United Nations Detention Unit in The Hague over four years after his trial had begun, many feared - and some hoped - that international criminal justice was experiencing some sort of death itself. Yet the Milos?evic? case, the first trial of a former head of state by a truly international criminal tribunal and one of the most complex and lengthy war crimes trials in history, stands for much in the development and the future of international criminal justice, both politically and legally. This book, written by the senior legal advisor working for the Trial Chamber, analyses the trial to determine what lessons can be learnt that will improve the fair and expeditious conduct of complex international criminal proceedings brought against former heads of state and senior political and military officials, and develops reforms for the future achievement of best practice in international criminal law. 606 $aTrials (Crimes against humanity)$zNetherlands$zHague 615 0$aTrials (Crimes against humanity) 676 $a345.05 700 $aBoas$b Gideon$0603637 801 0$bUkCbUP 801 1$bUkCbUP 906 $aBOOK 912 $a9910452089903321 996 $aThe Milos?evic? trial$92464066 997 $aUNINA LEADER 08172nam 2200517 450 001 9910495155003321 005 20231110221911.0 010 $a3-030-85248-2 035 $a(CKB)4100000012008386 035 $a(MiAaPQ)EBC6710562 035 $a(Au-PeEL)EBL6710562 035 $a(PPN)257350713 035 $a(EXLCZ)994100000012008386 100 $a20220513d2021 uy 0 101 0 $aeng 135 $aurcnu|||||||| 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 00$aFormal methods for industrial critical systems $e26th international conference, FMICS 2021, Paris, France, August 24-26, 2021 : proceedings /$fAlberto Lluch Lafuente, Anastasia Mavridou (editors) 210 1$aCham, Switzerland :$cSpringer,$d[2021] 210 4$d©2021 215 $a1 online resource (253 pages) 225 1 $aLecture Notes in Computer Science ;$vv.12863 311 $a3-030-85247-4 327 $aIntro -- Preface -- Organization -- Haunting Tales of Applied Formal Methods from Academia and Industry (Abstract of Invited Talk) -- Contents -- Verification -- Verification of Co-simulation Algorithms Subject to Algebraic Loops and Adaptive Steps -- 1 Introduction -- 2 Background -- 2.1 Simulation Units -- 2.2 Co-simulation Algorithms -- 2.3 Correct Co-simulation Algorithms -- 3 Related Work -- 4 Verifying Complex Co-simulation Algorithms -- 4.1 Verifying an Algorithm Using UPPAAL -- 4.2 Verifying Complex Simulation Scenarios in UPPAAL -- 4.3 Debugging Algorithm Errors -- 5 Validation -- 5.1 Motivation Example -- 5.2 Complex Scenario -- 6 Concluding Remarks -- References -- Automated Verification of Temporal Properties of Ladder Programs -- 1 Introduction -- 2 Introduction to Ladder Programming -- 3 Translation of Ladder Programs to WhyML -- 3.1 The Why3 Environment -- 3.2 Translation of Ladder Codes -- 3.3 The Ladder Loop, and the Encoding of Timing Charts -- 4 Implementation and Experimental Results -- 4.1 Overview of the Approach -- 4.2 Results on Correct Code -- 4.3 Results on Incorrect Code -- 5 Discussions, Related Work and Future Work -- References -- Spatial Model Checking for Smart Stations -- 1 Introduction and Outline -- 2 Industrial Context and Case Study: Station Lighting -- 3 Challenges in User-Centric Design of Smart Stations -- 4 Methodology -- 4.1 Spatial Model Checking -- 4.2 Statistical Spatio-Temporal Model Checking -- 5 Conclusion and Outlook -- References -- Program Safety and Education -- Parametric Faults in Safety Critical Programs -- 1 Introduction -- 2 Background -- 3 Identifying Incorrect Parameters -- 4 Case Study -- 5 Discussion -- 6 Related Works -- 7 Conclusion -- References -- Modular Transformation of Java Exceptions Modulo Errors -- 1 Introduction -- 2 Background -- 2.1 Abrupt Termination -- 2.2 VerCors. 327 $a3 Related Work -- 4 Semantics of Exceptions -- 4.1 Errors and Sources of Errors -- 4.2 Ideal Semantics -- 4.3 Semantics Modulo Errors -- 5 The finally Encoding Problem -- 5.1 Candidate Encodings -- 6 Evaluation -- 6.1 Common Exception Patterns in Commercial Software -- 6.2 Verification with VerCors -- 7 Discussion -- 7.1 Backend Requirements -- 7.2 Performance -- 8 Conclusion -- References -- On Education and Training in Formal Methods for Industrial Critical Systems -- 1 Introduction -- 2 Terminology -- 3 Roles in Formal Methods for Industrial Critical Systems: [Engineer] and [Engineer] -- 3.1 FMICS Roles and Activities -- 3.2 Consequences on Education and Training -- 4 Learning Objectives: vs. -- 5 Curriculum and Course Construction -- 6 Exemplary Implementation -- 7 Conclusion -- References -- (Event-)B Modeling and Validation -- Improving SMT Solver Integrations for the Validation of B and Event-B Models -- 1 Introduction -- 2 Former Z3 Integration -- 2.1 High-Level Translation -- 2.2 Workflow -- 3 New Z3 Integration -- 3.1 High-Level Translation -- 3.2 New Workflow -- 4 Empirical Evaluation -- 4.1 Weaknesses of the Integration of Z3 -- 4.2 Strengths of the Integration of Z3 -- 4.3 Symbolic Model Checking -- 5 Related Work -- 6 Future Work -- 7 Conclusion -- References -- Standard Conformance-by-Construction with Event-B -- 1 Introduction -- 2 Certification and Conformance -- 3 Event-B -- 3.1 Contexts and Machines (Tables1b and 1c) -- 3.2 Event-B Extensions with Theories -- 4 Case Study: ARINC 661 + Multi-purpose Interactive Application -- 4.1 ARINC 661 Standard Specification: An Extract -- 4.2 Multi-purpose Interactive Application and Weather Radar System -- 5 Standards Formalised as Ontologies ((1) on Fig.2) -- 6 Our Approach -- 6.1 Domain Standards as Ontology-Based Theories ((2) on Fig.2) -- 6.2 Standard Theory Instantiation ((3) on Fig.2). 327 $a6.3 Model Annotation for Conformance ((4) on Fig.2) -- 7 Standard Conformance-by-Construction: The Case of ARINC 661 -- 7.1 ARINC 661 Standard Formalisation ((2) on Fig.2) -- 7.2 System-Specific Concepts Describing WXR Widgets ((3) on Fig.2) -- 7.3 Annotated Event-B Model of WXR Application ((4) on Fig.2) -- 8 Assessment -- 9 Conclusion -- References -- Formal Analysis -- Randomized Reachability Analysis in Uppaal: Fast Error Detection in Timed Systems -- 1 Introduction -- 2 Randomized Reachability Analysis -- 3 New Results on Herschel-Planck -- 4 More Schedulability -- 5 Gossiping Girls -- 6 Scalability Experiments -- 7 Conclusion -- 8 Future Work -- References -- Verifying the Mathematical Library of an UAV Autopilot with Frama-C -- 1 Introduction -- 2 The Paparazzi Autopilot -- 3 Proving the Absence of Runtime Errors -- 4 Functional Verification Using Automatic Provers -- 5 Functional Verification Using Interactive Provers -- 6 Conclusion -- References -- Formal Analysis of the UNISIG Safety Application Intermediate Sub-layer -- 1 Introduction -- 2 Background -- 3 The Model -- 4 The Analysis -- 5 Conclusion -- References -- Tools -- ProB2-UI: A Java-Based User Interface for ProB -- 1 Introduction and Motivation -- 2 Features of ProB2-UI -- 3 Related Work -- 4 Conclusion -- References -- Intrepid: A Scriptable and Cloud-Ready SMT-Based Model Checker -- 1 Introduction -- 2 Constructing Models -- 2.1 Translating Industrially-Relevant Models -- 3 Simulating Models -- 4 Model Checking -- 4.1 A Comparison of the Engines -- 5 Sample Applications -- 5.1 Equivalence Checking for Clock-Gating -- 5.2 Automated Test Generation of MC/DC -- 6 A REST API for Model Checking -- 7 Conclusion -- References -- Merit and Blame Assignment with Kind 2 -- 1 Introduction -- 2 Running Example -- 3 The New Features -- 4 Implementation Details -- References. 327 $aTest Generation and Probabilistic Verification -- PSY-TaLiRo: A Python Toolbox for Search-Based Test Generation for Cyber-Physical Systems -- 1 Introduction -- 2 Architecture -- 3 Interface -- 3.1 System Under Test (SUT) -- 3.2 Specifications -- 3.3 Optimizers -- 3.4 Options -- 4 Examples -- 4.1 MATLAB/Simulink -- 4.2 PX4 -- 5 Conclusions -- References -- Probabilistic Verification for Reliability of a Two-by-Two Network-on-Chip System -- 1 Introduction -- 2 Motivation -- 3 Concrete Formal Model for NoC -- 4 Need for Abstraction -- 4.1 Predicate Abstraction to Simplify Complex Data Structures -- 4.2 Probabilistic Choice Abstraction -- 4.3 Boolean Queue Abstraction -- 5 Results -- 5.1 Every Other Cycle Flit Injection -- 5.2 Burst Flit Injection -- 5.3 Minimizing PSN with Flit Generation Pattern -- 5.4 Results Summary and Discussion -- 6 Conclusion -- References -- Author Index. 410 0$aLecture Notes in Computer Science 606 $aFormal methods (Computer science)$vCongresses 606 $aSoftware engineering$vCongresses 606 $aComputer programs$xVerification$vCongresses 615 0$aFormal methods (Computer science) 615 0$aSoftware engineering 615 0$aComputer programs$xVerification 676 $a004.0151 702 $aLluch Lafuente$b Alberto 702 $aMavridou$b Anastasia 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910495155003321 996 $aFormal Methods for Industrial Critical Systems$91921860 997 $aUNINA LEADER 02120nam 2200565 450 001 9910797527803321 005 20230807193215.0 010 $a1-55152-603-4 035 $a(CKB)3710000000476257 035 $a(EBL)4414207 035 $a(SSID)ssj0001570282 035 $a(PQKBManifestationID)16220555 035 $a(PQKBTitleCode)TC0001570282 035 $a(PQKBWorkID)14836057 035 $a(PQKB)11048933 035 $a(MiAaPQ)EBC4596327 035 $a(Au-PeEL)EBL4596327 035 $a(CaPaEBR)ebr11242309 035 $a(CaONFJC)MIL831656 035 $a(OCoLC)913612259 035 $a(EXLCZ)993710000000476257 100 $a20160824h20152015 uy 0 101 0 $aeng 135 $aur|n|---||||| 181 $ctxt 182 $cc 183 $acr 200 00$aFoucault against himself /$fFrancois Caillat ; foreword by Paul Rabinow ; featuring Leo Bersani, Georges Didi-Humberman, Arlette Farge, Geoffroy de Lagasnerie ; translated by David Homel 210 1$aVancouver, British Columbia :$cArsenal Pulp Press,$d2015. 210 4$d?2015 215 $a1 online resource (153 p.) 300 $aDescription based upon print version of record. 311 $a1-55152-602-6 327 $aContents; Foreword | Paul Rabinow ; Introduction | Francois Caillat; On the Perception of the Intolerable | Arlette Farge; Learning to Escape: (Meditations on Relational Modes) | Leo Bersani; Knowing When to Cut | Georges Didi-Huberman; What Does It Mean to Think? | Geoffroy de Lagasnerie; Contributors 330 $aEssays on Foucault reframing his legacy and building new ways of thinking about the struggle against society's mechanisms of domination. 676 $a194 702 $aCaillat$b Franc?ois 702 $aDidi-Huberman$b Georges 702 $aRabinow$b Paul 702 $aHomel$b David 702 $aFarge$b Arlette 702 $aBersani$b Leo 702 $aLagasnerie$b Geoffroy de 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910797527803321 996 $aFoucault against himself$93684823 997 $aUNINA