SOFSEM 2017: Theory and Practice of Computer Science : 43rd International Conference on Current Trends in Theory and Practice of Computer Science, Limerick, Ireland, January 16-20, 2017, Proceedings / / edited by Bernhard Steffen, Christel Baier, Mark van den Brand, Johann Eder, Mike Hinchey, Tiziana Margaria |
Edizione | [1st ed. 2017.] |
Pubbl/distr/stampa | Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017 |
Descrizione fisica | 1 online resource (XVIII, 526 p. 109 illus.) |
Disciplina | 004.015113 |
Collana | Theoretical Computer Science and General Issues |
Soggetto topico |
Algorithms
Information storage and retrieval systems Application software Software engineering Computer networks Artificial intelligence Information Storage and Retrieval Computer and Information Systems Applications Software Engineering Computer Communication Networks Artificial Intelligence |
ISBN | 3-319-51963-8 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Dependable and Optimal Cyber-Physical Systems -- Verifying Parametric Thread Creation -- Network Constructors: A Model for Programmable Matter -- Logical characterisations and compositionality of input-output conformance simulation -- A Linear-Time Branching-Time Spectrum of Behavioral Specification Theories -- Symbolic semantics for multiparty interactions in the link-calculus -- Different Speeds Suffice for Rendezvous of Two Agents on Arbitrary Graphs -- Deciding structural liveness of Petri nets -- Distributed Network Generation based on Preferential Attachment in ABS -- Completeness of Hoare Logic Relative to the Standard Model -- Configuration- and Residual-Based Transition Systems for Event Structures with Asymmetric Conflict -- Hardness of deriving invertible sequences from finite state machines -- A Graph-theoretical Characterisation of State Separation -- Selfish Transportation Games -- Decomposable Relaxation for Concurrent Data Structures -- Sufficient Conditions for a Connected Graph to have a Hamiltonian Path -- Enumerating Minimal Tropical Connected Sets -- Bamboo Garden Trimming Problem (Perpetual maintenance of machines with different attendance urgency factors) -- Exact quantum query complexity of EXACT_{k,l}^n -- Adjacent vertices can be hard to find by quantum walks -- Matrix semigroup freeness problems in SL(2,Z) -- Order-preserving 1-string representations of planar graphs -- How to Draw a Planarization -- Finding Largest Common Substructures of Molecules in Quadratic Time -- Lower Bounds for On-line Interval Coloring with Vector and Cardinality Constraints -- Parameterized and Exact Algorithms for Class Domination Coloring -- The Approximability of Partial Vertex Covers in Trees -- Longest Common Subsequence in at Least k Length Order-isomorphic Substrings -- Computing longest single-arm-gapped palindromes in a string -- Edit-Distance between Visibly Pushdown Languages -- Trends and Challenges in Predictive Analytics -- Model-driven Development in Practice: From Requirements to Code -- Webpage Menu Detection Based on DOM -- A Hybrid Model for Linking Multiple Social Identities across Heterogeneous Online Social Networks -- Eco Data Warehouse Design Through Logical Variability -- On Featured Transition Systems -- Domain-Specific Languages: A Systematic Mapping Study -- Characterising Malicious Software with High-Level Behavioural Patterns -- AErlang at work -- Software Systems Migration towards Cloud-native Architectures for SME-sized Software Vendors -- Using n-grams for the Automated Clustering of Structural Models. |
Record Nr. | UNINA-9910484047003321 |
Cham : , : Springer International Publishing : , : Imprint : Springer, , 2017 | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|
Software Process Improvement [[electronic resource] ] : 14th European Conference, EuroSPI 2007, Potsdam, Germany, September 26-28, 2007, Proceedings / / edited by Pekka Abrahamsson, Nathan Baddoo, Tiziana Margaria, Richard Messnarz |
Edizione | [1st ed. 2007.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
Descrizione fisica | 1 online resource (XI, 225 p.) |
Disciplina | 004.24 |
Collana | Programming and Software Engineering |
Soggetto topico |
Software engineering
Management information systems Computer science Computers and civilization Software Engineering/Programming and Operating Systems Software Engineering Management of Computing and Information Systems Computers and Society |
ISBN | 3-540-75381-8 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Software Process Improvement – EuroSPI 2007 Conference -- Enforcement, Alignment, Tailoring -- Tailoring and Introduction of the Rational Unified Process -- Maintaining a Large Process Model Aligned with a Process Standard: An Industrial Example -- Synergies Between the Common Criteria and Process Improvement -- Focus on SME Issues -- Determining Practice Achievement in Project Management Using a Two-Phase Questionnaire on Small and Medium Enterprises -- Using Practice Outcome Areas to Understand Perceived Value of CMMI Specific Practices for SMEs -- SPI with Lightweight Software Process Modeling in a Small Software Company -- Improvement Analysis and Empirical Studies -- A Practitioner Experiment in Understanding Software Process Improvement Using Systems Modular Analysis -- Organizing Improvement Work: A Longitudinal Case -- An Experiment with a Release Planning Method for Web Application Development -- New Avenues of SPI -- Defining a Legal Risk Management Strategy: Process, Legal Risk and Lifecycle -- iCharts: Charts for Software Process Improvement Value Management -- Organizational Learning Through Project Postmortem Reviews – An Explorative Case Study -- SPI Methodologies -- Modelling Software Processes as Human-Centered Adaptive Work Systems -- Performance Comparison of Software Complexity Metrics in an Open Source Project -- A Methodology for Identifying Critical Success Factors That Influence Software Process Improvement Initiatives: An Application in the Brazilian Software Industry -- Testing and Reliability -- Quality Impact of Introducing Component-Level Test Automation and Test-Driven Development -- The Impact of Test-Driven Development on Software Development Productivity — An Empirical Study -- Investigating the Software Fault Profile of Industrial Projects to Determine Process Improvement Areas: An Empirical Study. |
Record Nr. | UNISA-996465297903316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Software Process Improvement : 14th European Conference, EuroSPI 2007, Potsdam, Germany, September 26-28, 2007, Proceedings / / edited by Pekka Abrahamsson, Nathan Baddoo, Tiziana Margaria, Richard Messnarz |
Edizione | [1st ed. 2007.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
Descrizione fisica | 1 online resource (XI, 225 p.) |
Disciplina | 004.24 |
Collana | Programming and Software Engineering |
Soggetto topico |
Software engineering
Management information systems Computer science Computers and civilization Software Engineering/Programming and Operating Systems Software Engineering Management of Computing and Information Systems Computers and Society |
ISBN | 3-540-75381-8 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Software Process Improvement – EuroSPI 2007 Conference -- Enforcement, Alignment, Tailoring -- Tailoring and Introduction of the Rational Unified Process -- Maintaining a Large Process Model Aligned with a Process Standard: An Industrial Example -- Synergies Between the Common Criteria and Process Improvement -- Focus on SME Issues -- Determining Practice Achievement in Project Management Using a Two-Phase Questionnaire on Small and Medium Enterprises -- Using Practice Outcome Areas to Understand Perceived Value of CMMI Specific Practices for SMEs -- SPI with Lightweight Software Process Modeling in a Small Software Company -- Improvement Analysis and Empirical Studies -- A Practitioner Experiment in Understanding Software Process Improvement Using Systems Modular Analysis -- Organizing Improvement Work: A Longitudinal Case -- An Experiment with a Release Planning Method for Web Application Development -- New Avenues of SPI -- Defining a Legal Risk Management Strategy: Process, Legal Risk and Lifecycle -- iCharts: Charts for Software Process Improvement Value Management -- Organizational Learning Through Project Postmortem Reviews – An Explorative Case Study -- SPI Methodologies -- Modelling Software Processes as Human-Centered Adaptive Work Systems -- Performance Comparison of Software Complexity Metrics in an Open Source Project -- A Methodology for Identifying Critical Success Factors That Influence Software Process Improvement Initiatives: An Application in the Brazilian Software Industry -- Testing and Reliability -- Quality Impact of Introducing Component-Level Test Automation and Test-Driven Development -- The Impact of Test-Driven Development on Software Development Productivity — An Empirical Study -- Investigating the Software Fault Profile of Industrial Projects to Determine Process Improvement Areas: An Empirical Study. |
Record Nr. | UNINA-9910484578703321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|
Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I / / edited by Axel Legay, Tiziana Margaria |
Edizione | [1st ed. 2017.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2017 |
Descrizione fisica | 1 online resource (XXIV, 609 p. 152 illus.) |
Disciplina | 005.14 |
Collana | Theoretical Computer Science and General Issues |
Soggetto topico |
Computer science
Algorithms Software engineering Compilers (Computer programs) Machine theory Computer Science Logic and Foundations of Programming Software Engineering Theory of Computation Compilers and Interpreters Formal Languages and Automata Theory |
ISBN | 3-662-54577-2 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Talk -- Validation, Synthesis and Optimization for Cyber-Physical Systems -- Verification Techniques -- An Abstraction Technique For Parameterized Model Checking of Leader Election Protocols: Application to FTSP -- Combining String Abstract Domains for JavaScript Analysis: An Evaluation.-Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF -- Bounded Quantifier Instantiation for Checking Inductive Invariants -- Proving Termination through Conditional Termination.-Efficient Certified Resolution Proof Checking -- Precise Widening Operators for Proving Termination by Abstract Interpretation -- Automatic Verification of Finite Precision Implementations of Linear Controllers -- Learning -- Learning Symbolic Automata -- ML for ML: Learning Cost Semantics by Experiment -- A Novel Learning Algorithm for Buchi Automata based on Family of DFAs and Classification Trees -- Synthesis -- Hierarchical Network Formation Games -- Synthesis of Recursive ADT Transformers from Reusable Templates -- Counterexample-Guided Model Synthesis -- Interpolation-Based GR(1) Assumptions Refinement -- Connecting Program Synthesis and Reachability: Automatic Program Repair using Test-Input Generation -- Scaling Enumerative Program Synthesis via Divide and Conquer -- Towards Parallel Boolean Functional Synthesis -- Encodings of Bounded Synthesis -- Tools -- HQSpre - An Effective Preprocessor for QBF and DQBF -- RPP: Automatic Proof of Relational Properties by Self-Composition -- autoCode4: Structural Controller Synthesis -- Automata -- Lazy Automata Techniques for WS1S -- From LTL and limit-deterministic Büchi automata to deterministic parity automata -- Index appearance record for transforming Rabin automata into parity automata -- Minimization of Visibly Pushdown Automata Using Partial Max-SAT -- Concurrency and Bisimulation -- CSimpl: a Framework for the Verification of Concurrent Programs using Rely-Guarante -- Fair Termination for Parameterized Probabilistic Concurrent Systems -- Forward Bisimulations for Nondeterministic Symbolic Finite Automata -- Up-To Techniques for Weighted Systems -- Hybrid Systems -- Rigorous Simulation-Based Analysis of Linear Hybrid Systems -- HARE: A Hybrid Abstraction Refinement Engine for Verifying Non-Linear Hybrid Automata -- Counterexample-guided Refinement of Template Polyhedra. . |
Record Nr. | UNISA-996466187103316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2017 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part II / / edited by Axel Legay, Tiziana Margaria |
Edizione | [1st ed. 2017.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2017 |
Descrizione fisica | 1 online resource (XXIV, 411 p. 88 illus.) |
Disciplina | 005.1 |
Collana | Theoretical Computer Science and General Issues |
Soggetto topico |
Computer science
Algorithms Software engineering Compilers (Computer programs) Machine theory Computer Science Logic and Foundations of Programming Software Engineering Theory of Computation Compilers and Interpreters Formal Languages and Automata Theory |
ISBN | 3-662-54580-2 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Security -- Static Detection of DoS Vulnerabilities in Programs that use Regular Expressions -- Discriminating Traces with Time -- Directed Automated Memory Performance Testing -- Context-bounded Analysis for POWER -- Run-Time Verification and Logic. -Rewriting-Based Runtime Verification of Alternation-Free HyperLTL Formulas -- Almost Event-Rate Independent Monitoring of Metric Temporal Logic -- Optimal Translation of LTL to Limit Deterministic Automata -- Quantitative Systems -- Sequential Convex Programming for the Efficient Verification of Parametric MDPs -- JANI: Quantitative Model and Tool Interaction -- Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic Faults -- Long-run Rewards for Markov Automata -- SAT and SMT -- HiFrog: SMT-based Function Summarization for Software Verification -- Congruence Closure with Free Variables -- On Optimization Modulo Theories, MaxSMT and Sorting Networks. - The automatic detection of token structures and invariants using SAT checking -- Maximizing the Conditional Expected Reward for Reaching the Goal. -ARES: Adaptive Receding-Horizon Synthesis of Optimal Plans. - FlyFast: A Mean Field Model Checker. -ERODE: A Tool for the Evaluation and Reduction of Ordinary Differential Equations -- SV COMP -- Software Verification with Validation of Results (Report on SV-COMP 2017) -- AProVE: Proving and Disproving Termination of Memory-Manipulating C Programs (Competition Contribution) -- CPA-BAM-BnB: Block-Abstraction Memoization and Region-based Memory Models for Predicate Abstractions (Competition Contribution) -- DepthK: A k-Induction Verifier Based on Invariant Inference for C Programs (Competition Contribution) -- Forester: From Heap Shapes to Automata Predicates (Competition Contribution) -- HipTNT+: A Termination and Non-termination Analyzer by Second-order Abduction (Competition Contribution) -- Lazy-CSeq 2.0: Combining Lazy Sequentialization with Abstract Interpretation (Competition Contribution) -- Skink: Static Analysis of LLVM Intermediate Representation (Competition contribution) -- Symbiotic 4: Beyond Reachability (Competition Contribution) -- Optimizing and Caching SMT Queries in SymDIVINE (Competition Contribution) -- Ultimate Automizer with an On-demand Construction of Floyd-Hoare Automata (Competition Contribution) -- Ultimate Taipan: Trace Abstraction and Abstract Interpretation (Competition Contribution) -- VeriAbs : Verification by Abstraction (Competition Contribution). . |
Record Nr. | UNISA-996466185203316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2017 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Tools and Algorithms for the Construction and Analysis of Systems : 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part II / / edited by Axel Legay, Tiziana Margaria |
Edizione | [1st ed. 2017.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2017 |
Descrizione fisica | 1 online resource (XXIV, 411 p. 88 illus.) |
Disciplina | 005.1 |
Collana | Theoretical Computer Science and General Issues |
Soggetto topico |
Computer science
Algorithms Software engineering Compilers (Computer programs) Machine theory Computer Science Logic and Foundations of Programming Software Engineering Theory of Computation Compilers and Interpreters Formal Languages and Automata Theory |
ISBN | 3-662-54580-2 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Security -- Static Detection of DoS Vulnerabilities in Programs that use Regular Expressions -- Discriminating Traces with Time -- Directed Automated Memory Performance Testing -- Context-bounded Analysis for POWER -- Run-Time Verification and Logic. -Rewriting-Based Runtime Verification of Alternation-Free HyperLTL Formulas -- Almost Event-Rate Independent Monitoring of Metric Temporal Logic -- Optimal Translation of LTL to Limit Deterministic Automata -- Quantitative Systems -- Sequential Convex Programming for the Efficient Verification of Parametric MDPs -- JANI: Quantitative Model and Tool Interaction -- Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic Faults -- Long-run Rewards for Markov Automata -- SAT and SMT -- HiFrog: SMT-based Function Summarization for Software Verification -- Congruence Closure with Free Variables -- On Optimization Modulo Theories, MaxSMT and Sorting Networks. - The automatic detection of token structures and invariants using SAT checking -- Maximizing the Conditional Expected Reward for Reaching the Goal. -ARES: Adaptive Receding-Horizon Synthesis of Optimal Plans. - FlyFast: A Mean Field Model Checker. -ERODE: A Tool for the Evaluation and Reduction of Ordinary Differential Equations -- SV COMP -- Software Verification with Validation of Results (Report on SV-COMP 2017) -- AProVE: Proving and Disproving Termination of Memory-Manipulating C Programs (Competition Contribution) -- CPA-BAM-BnB: Block-Abstraction Memoization and Region-based Memory Models for Predicate Abstractions (Competition Contribution) -- DepthK: A k-Induction Verifier Based on Invariant Inference for C Programs (Competition Contribution) -- Forester: From Heap Shapes to Automata Predicates (Competition Contribution) -- HipTNT+: A Termination and Non-termination Analyzer by Second-order Abduction (Competition Contribution) -- Lazy-CSeq 2.0: Combining Lazy Sequentialization with Abstract Interpretation (Competition Contribution) -- Skink: Static Analysis of LLVM Intermediate Representation (Competition contribution) -- Symbiotic 4: Beyond Reachability (Competition Contribution) -- Optimizing and Caching SMT Queries in SymDIVINE (Competition Contribution) -- Ultimate Automizer with an On-demand Construction of Floyd-Hoare Automata (Competition Contribution) -- Ultimate Taipan: Trace Abstraction and Abstract Interpretation (Competition Contribution) -- VeriAbs : Verification by Abstraction (Competition Contribution). . |
Record Nr. | UNINA-9910484283703321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2017 | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|
Tools and Algorithms for the Construction and Analysis of Systems : 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I / / edited by Axel Legay, Tiziana Margaria |
Edizione | [1st ed. 2017.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2017 |
Descrizione fisica | 1 online resource (XXIV, 609 p. 152 illus.) |
Disciplina | 005.14 |
Collana | Theoretical Computer Science and General Issues |
Soggetto topico |
Computer science
Algorithms Software engineering Compilers (Computer programs) Machine theory Computer Science Logic and Foundations of Programming Software Engineering Theory of Computation Compilers and Interpreters Formal Languages and Automata Theory |
ISBN | 3-662-54577-2 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Talk -- Validation, Synthesis and Optimization for Cyber-Physical Systems -- Verification Techniques -- An Abstraction Technique For Parameterized Model Checking of Leader Election Protocols: Application to FTSP -- Combining String Abstract Domains for JavaScript Analysis: An Evaluation.-Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF -- Bounded Quantifier Instantiation for Checking Inductive Invariants -- Proving Termination through Conditional Termination.-Efficient Certified Resolution Proof Checking -- Precise Widening Operators for Proving Termination by Abstract Interpretation -- Automatic Verification of Finite Precision Implementations of Linear Controllers -- Learning -- Learning Symbolic Automata -- ML for ML: Learning Cost Semantics by Experiment -- A Novel Learning Algorithm for Buchi Automata based on Family of DFAs and Classification Trees -- Synthesis -- Hierarchical Network Formation Games -- Synthesis of Recursive ADT Transformers from Reusable Templates -- Counterexample-Guided Model Synthesis -- Interpolation-Based GR(1) Assumptions Refinement -- Connecting Program Synthesis and Reachability: Automatic Program Repair using Test-Input Generation -- Scaling Enumerative Program Synthesis via Divide and Conquer -- Towards Parallel Boolean Functional Synthesis -- Encodings of Bounded Synthesis -- Tools -- HQSpre - An Effective Preprocessor for QBF and DQBF -- RPP: Automatic Proof of Relational Properties by Self-Composition -- autoCode4: Structural Controller Synthesis -- Automata -- Lazy Automata Techniques for WS1S -- From LTL and limit-deterministic Büchi automata to deterministic parity automata -- Index appearance record for transforming Rabin automata into parity automata -- Minimization of Visibly Pushdown Automata Using Partial Max-SAT -- Concurrency and Bisimulation -- CSimpl: a Framework for the Verification of Concurrent Programs using Rely-Guarante -- Fair Termination for Parameterized Probabilistic Concurrent Systems -- Forward Bisimulations for Nondeterministic Symbolic Finite Automata -- Up-To Techniques for Weighted Systems -- Hybrid Systems -- Rigorous Simulation-Based Analysis of Linear Hybrid Systems -- HARE: A Hybrid Abstraction Refinement Engine for Verifying Non-Linear Hybrid Automata -- Counterexample-guided Refinement of Template Polyhedra. . |
Record Nr. | UNINA-9910484283903321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2017 | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|
Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : 7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001 Proceedings / / edited by Tiziana Margaria, Wang Yi |
Edizione | [1st ed. 2001.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 |
Descrizione fisica | 1 online resource (XIV, 594 p.) |
Disciplina | 004.2/11 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Software engineering
Computer logic Computer communication systems Algorithms Software Engineering/Programming and Operating Systems Logics and Meanings of Programs Software Engineering Computer Communication Networks Algorithm Analysis and Problem Complexity |
ISBN | 3-540-45319-9 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Contributions -- Branching vs. Linear Time: Final Showdown -- Propositional Reasoning -- Symbolic Verification -- Language Containment Checking with Nondeterministic BDDs -- Satisfiability Checking Using Boolean Expression Diagrams -- A Library for Composite Symbolic Representations -- Infinite State Systems: Deduction and Abstraction -- Synthesis of Linear Ranking Functions -- Automatic Deductive Verification with Invisible Invariants -- Incremental Verification by Abstraction -- A Technique for Invariant Generation -- Application of Model Checking Techniques -- Model Checking Syllabi and Student Careers -- Verification of Vortex Workflows -- Parameterized Verification of Multithreaded Software Libraries -- Timed and Probabilistic Systems -- Efficient Guiding Towards Cost-Optimality in UPPAAL -- Linear Parametric Model Checking of Timed Automata -- Abstraction in Probabilistic Process Algebra -- First Passage Time Analysis of Stochastic Process Algebra Using Partial Orders -- Hardware: Design and Verification -- Hardware/Software Co-design Using Functional Languages -- Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors -- Software Verification -- Boolean and Cartesian Abstraction for Model Checking C Programs -- Finding Feasible Counter-examples when Model Checking Abstracted Java Programs -- The loop Compiler for Java and JML -- Symbolic Verification -- Searching Powerset Automata by Combining Explicit-State and Symbolic Model Checking -- Saturation: An Efficient Iteration Strategy for Symbolic State—Space Generation -- Testing: Techniques and Tools -- Automated Test Generation from Timed Automata -- Testing an Intentional Naming Scheme Using Genetic Algorithms -- Building a Tool for the Analysis and Testing of Web Applications: Problems and Solutions -- TATOO: Testing and Analysis Tool for Object-Oriented Software -- Implementation Techniques -- Implementing a Multi-valued Symbolic Model Checker -- Is There a Best Symbolic Cycle-Detection Algorithm? -- Combining Structural and Enumerative Techniques for the Validation of Bounded Petri Nets -- A Sweep-Line Method for State Space Exploration -- Semantics and Compositional Verification -- Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams -- Simulation Revisited -- Compositional Message Sequence Charts -- An Automata Based Interpretation of Live Sequence Charts -- Logics and Model-Checking -- Coverage Metrics for Temporal Logic Model Checking -- Parallel Model Checking for the Alternation Free ?-Calculus -- Model Checking CTL*[DC] -- ETAPS Tool Demonstration -- CPN/Tools: A Tool for Editing and Simulating Coloured Petri Nets ETAPS Tool Demonstration Related to TACAS -- The ASM Workbench: A Tool Environment for Computer-Aided Analysis and Validation of Abstract State Machine Models -- The Erlang Verification Tool. |
Record Nr. | UNISA-996465708203316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|
Tools and Algorithms for the Construction and Analysis of Systems : 7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001 Proceedings / / edited by Tiziana Margaria, Wang Yi |
Edizione | [1st ed. 2001.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 |
Descrizione fisica | 1 online resource (XIV, 594 p.) |
Disciplina | 004.2/11 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Software engineering
Computer logic Computer communication systems Algorithms Software Engineering/Programming and Operating Systems Logics and Meanings of Programs Software Engineering Computer Communication Networks Algorithm Analysis and Problem Complexity |
ISBN | 3-540-45319-9 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Contributions -- Branching vs. Linear Time: Final Showdown -- Propositional Reasoning -- Symbolic Verification -- Language Containment Checking with Nondeterministic BDDs -- Satisfiability Checking Using Boolean Expression Diagrams -- A Library for Composite Symbolic Representations -- Infinite State Systems: Deduction and Abstraction -- Synthesis of Linear Ranking Functions -- Automatic Deductive Verification with Invisible Invariants -- Incremental Verification by Abstraction -- A Technique for Invariant Generation -- Application of Model Checking Techniques -- Model Checking Syllabi and Student Careers -- Verification of Vortex Workflows -- Parameterized Verification of Multithreaded Software Libraries -- Timed and Probabilistic Systems -- Efficient Guiding Towards Cost-Optimality in UPPAAL -- Linear Parametric Model Checking of Timed Automata -- Abstraction in Probabilistic Process Algebra -- First Passage Time Analysis of Stochastic Process Algebra Using Partial Orders -- Hardware: Design and Verification -- Hardware/Software Co-design Using Functional Languages -- Automatic Abstraction of Memories in the Formal Verification of Superscalar Microprocessors -- Software Verification -- Boolean and Cartesian Abstraction for Model Checking C Programs -- Finding Feasible Counter-examples when Model Checking Abstracted Java Programs -- The loop Compiler for Java and JML -- Symbolic Verification -- Searching Powerset Automata by Combining Explicit-State and Symbolic Model Checking -- Saturation: An Efficient Iteration Strategy for Symbolic State—Space Generation -- Testing: Techniques and Tools -- Automated Test Generation from Timed Automata -- Testing an Intentional Naming Scheme Using Genetic Algorithms -- Building a Tool for the Analysis and Testing of Web Applications: Problems and Solutions -- TATOO: Testing and Analysis Tool for Object-Oriented Software -- Implementation Techniques -- Implementing a Multi-valued Symbolic Model Checker -- Is There a Best Symbolic Cycle-Detection Algorithm? -- Combining Structural and Enumerative Techniques for the Validation of Bounded Petri Nets -- A Sweep-Line Method for State Space Exploration -- Semantics and Compositional Verification -- Assume-Guarantee Based Compositional Reasoning for Synchronous Timing Diagrams -- Simulation Revisited -- Compositional Message Sequence Charts -- An Automata Based Interpretation of Live Sequence Charts -- Logics and Model-Checking -- Coverage Metrics for Temporal Logic Model Checking -- Parallel Model Checking for the Alternation Free ?-Calculus -- Model Checking CTL*[DC] -- ETAPS Tool Demonstration -- CPN/Tools: A Tool for Editing and Simulating Coloured Petri Nets ETAPS Tool Demonstration Related to TACAS -- The ASM Workbench: A Tool Environment for Computer-Aided Analysis and Validation of Abstract State Machine Models -- The Erlang Verification Tool. |
Record Nr. | UNINA-9910768474203321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2001 | ||
![]() | ||
Lo trovi qui: Univ. Federico II | ||
|
Tools and Algorithms for the Construction and Analysis of Systems [[electronic resource] ] : Second International Workshop, TACAS '96, Passau, Germany, March 27 - 29, 1996, Proceedings. / / edited by Tiziana Margaria, Bernhard Steffen |
Edizione | [1st ed. 1996.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1996 |
Descrizione fisica | 1 online resource (XIII, 443 p.) |
Disciplina | 004.2/1 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Computers
Operating systems (Computers) Computer logic Software engineering Computer communication systems Theory of Computation Operating Systems Logics and Meanings of Programs Software Engineering Computer Communication Networks |
ISBN | 3-540-49874-5 |
Formato | Materiale a stampa ![]() |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Early fault detection tools -- Kleene algebra with tests and commutativity conditions -- Managing proofs -- An analyzer for message sequence charts -- Relation-algebraic analysis of Petri nets with RELVIEW -- Efficient search as a means of executing specifications -- An improvement of McMillan's unfolding algorithm -- Efficient local model-checking for fragments of the modal ?-calculus -- Test generation with inputs, outputs, and quiescence -- Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR -- Automatic compositional verification of some Security properties -- Permutable agents in process algebras -- Strategy construction in infinite games with Streett and Rabin chain winning conditions -- Timed Condition/Event systems: A framework for modular discrete models of chemical plants and verification of their real-time discrete control -- Formal verification of a partial-order reduction technique for model checking -- Fully automatic verification and error detection for parameterized iterative sequential circuits -- Priorities for modeling and verifying distributed systems -- Games and modal mu-calculus -- Generic system support for deductive program development -- Extending promela and spin for real time -- Reactive EFSMs — Reactive Promela/RSPIN -- Probabilistic duration automata for analyzing real-time systems -- The Concurrency Factory software development environment -- The Fc2Tools set (tool demonstration) -- PEP — more than a Petri Net tool -- Rapid prototyping for an assertional specification language -- cTc — A tool supporting the construction of cTLA-Specifications -- A tool for proving invariance properties of concurrent systems automatically -- Using the constraint language toupie for “Software Cost Reduction” specification analysis -- A constraint-oriented Service Creation Environment -- DFA&OPT-MetaFrame: A tool kit for program analysis and optimization -- A construction and analysis tool based on the stochastic process algebra TIPP -- Uppaal in 1995. |
Record Nr. | UNISA-996465574203316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1996 | ||
![]() | ||
Lo trovi qui: Univ. di Salerno | ||
|