This bookconstitutes the refereed proceedings of the 12th International Conference on IntegratedFormal Methods, IFM 2016, held in Reykjavik, Iceland, in June 2016. The 33 paperspresented in this volume were carefully reviewed and selected from 99submissions. They were organized in topical sections named: invitedcontributions; program verification; probabilistic systems; concurrency; safetyand liveness; model learning; SAT and SMT solving; testing; theorem proving andconstraint satisfaction; case studies.
This bookconstitutes the refereed proceedings of the 12th International Conference on IntegratedFormal Methods, IFM 2016, held in Reykjavik, Iceland, in June 2016. The 33 paperspresented in this volume were carefully reviewed and selected from 99submissions. They were organized in topical sections named: invitedcontributions; program verification; probabilistic systems; concurrency; safetyand liveness; model learning; SAT and SMT solving; testing; theorem proving andconstraint satisfaction; case studies.
Invited Contributions.- Can Formal MethodsImprove the Efficiency of Code Reviews.-Symbolic Computation and AutomatedReasoning for Program Analysis.- Program verification.- On Type CheckingDelta-Oriented Product Lines.- Verifying a priority scheduler for an SCJruntime environment.- Why Just Boogie? Translating Between Intermediate VerificationLanguages.- Probabilistic systems.- Statistical Approximation of OptimalSchedulers for Probabilistic Timed Automata.- Probabilistic Formal Analysis ofApp Usage to Inform Redesign.- Extension of PRISM by Synthesis of OptimalTimeouts in Fixed-Delay CTMC.- Concurrency.- Monitoring Multi-threaded Component-BasedSystems.- A Generalised Theory of Interface Automata, Component Compatibility andError.- On Implementing a Monitor-Oriented Programming Framework for ActorSystems.- Towards a Thread-Local Proof Technique for Starvation Freedom.- Reasoningabout Inheritance and Unrestricted Reuse in Object-Oriented Concurrent Systems.-A Formal Model of the Safety-Critical Java Level 2 Paradigm.- Safety andliveness.- Deciding Monadic Second Order Logic over omega-words by Specialized FiniteAutomata.- Property Preservation for Extension Patterns of State TransitionDiagrams.- Symbolic Reachability Analysis of B through ProB and LTSmin.- Modellearning.- Enhancing Automata Learning by Log-Based Metrics.- Refactoring ofLegacy Software using Model Learning and Equivalence Checking: an IndustrialExperience Report.- On Robust Malware Classifiers by Verifying UnwantedBehaviours.- SAT and SMT solving.- Efficient Deadlock-Freedom Checking usingLocal Analysis and SAT Solving.- SMT Solvers for Validation of B and Event-Bmodels.- Avoiding Medication Conflicts for Patients with Multimorbidities.- Testing.-Temporal Random Testing for Spark Streaming.- Combining Static Analysis andTesting for Deadlock Detection.- Fuzzing JavaScript Engine APIs.- Theoremproving and constraint satisfaction.- A Component-based Approach to HybridSystemsSafety Verification.- Verifying Pointer Programs using Separation Logicand Invariant Based Programming in Isabelle.- A Constraint Satisfaction Methodfor Configuring Non-Local Service Interfaces.- Case studies.- Rule-basedConsistency Checking of Railway Infrastructure Designs.- Formal Verification ofSafety PLC Based Control Software.- Enabling Static Driver Verifier usingMicrosoft Azure.
Invited Contributions.- Can Formal MethodsImprove the Efficiency of Code Reviews.-Symbolic Computation and AutomatedReasoning for Program Analysis.- Program verification.- On Type CheckingDelta-Oriented Product Lines.- Verifying a priority scheduler for an SCJruntime environment.- Why Just Boogie? Translating Between Intermediate VerificationLanguages.- Probabilistic systems.- Statistical Approximation of OptimalSchedulers for Probabilistic Timed Automata.- Probabilistic Formal Analysis ofApp Usage to Inform Redesign.- Extension of PRISM by Synthesis of OptimalTimeouts in Fixed-Delay CTMC.- Concurrency.- Monitoring Multi-threaded Component-BasedSystems.- A Generalised Theory of Interface Automata, Component Compatibility andError.- On Implementing a Monitor-Oriented Programming Framework for ActorSystems.- Towards a Thread-Local Proof Technique for Starvation Freedom.- Reasoningabout Inheritance and Unrestricted Reuse in Object-Oriented Concurrent Systems.-A Formal Model of the Safety-Critical Java Level 2 Paradigm.- Safety andliveness.- Deciding Monadic Second Order Logic over omega-words by Specialized FiniteAutomata.- Property Preservation for Extension Patterns of State TransitionDiagrams.- Symbolic Reachability Analysis of B through ProB and LTSmin.- Modellearning.- Enhancing Automata Learning by Log-Based Metrics.- Refactoring ofLegacy Software using Model Learning and Equivalence Checking: an IndustrialExperience Report.- On Robust Malware Classifiers by Verifying UnwantedBehaviours.- SAT and SMT solving.- Efficient Deadlock-Freedom Checking usingLocal Analysis and SAT Solving.- SMT Solvers for Validation of B and Event-Bmodels.- Avoiding Medication Conflicts for Patients with Multimorbidities.- Testing.-Temporal Random Testing for Spark Streaming.- Combining Static Analysis andTesting for Deadlock Detection.- Fuzzing JavaScript Engine APIs.- Theoremproving and constraint satisfaction.- A Component-based Approach to HybridSystemsSafety Verification.- Verifying Pointer Programs using Separation Logicand Invariant Based Programming in Isabelle.- A Constraint Satisfaction Methodfor Configuring Non-Local Service Interfaces.- Case studies.- Rule-basedConsistency Checking of Railway Infrastructure Designs.- Formal Verification ofSafety PLC Based Control Software.- Enabling Static Driver Verifier usingMicrosoft Azure.
Es gelten unsere Allgemeinen Geschäftsbedingungen: www.buecher.de/agb
Impressum
www.buecher.de ist ein Internetauftritt der buecher.de internetstores GmbH
Geschäftsführung: Monica Sawhney | Roland Kölbl | Günter Hilger
Sitz der Gesellschaft: Batheyer Straße 115 - 117, 58099 Hagen
Postanschrift: Bürgermeister-Wegele-Str. 12, 86167 Augsburg
Amtsgericht Hagen HRB 13257
Steuernummer: 321/5800/1497
