Automated Technology for Verification and Analysis : 7th International Symposium, ATVA 2009, Macao, China, October 14-16, 2009 ; Proceedings / / Zhiming Liu, Anders P. Ravn (eds.) |
Edizione | [1st ed. 2009.] |
Pubbl/distr/stampa | Berlin ; ; Heidelberg, : Springer-Verlag, c2009 |
Descrizione fisica | 1 online resource (XI, 414 p.) |
Disciplina | 004n/a |
Altri autori (Persone) |
LiuZhiming <1961->
RavnAnders P |
Collana | Lecture notes in computer science |
Soggetto topico |
Artificial intelligence
Automatic theorem proving |
ISBN | 3-642-04761-0 |
Classificazione |
DAT 286f
DAT 325f DAT 704f SS 4800 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Talks -- Verifying VLSI Circuits -- 3-Valued Abstraction for (Bounded) Model Checking -- Local Search in Model Checking -- State Space Reduction -- Exploring the Scope for Partial Order Reduction -- State Space Reduction of Linear Processes Using Control Flow Reconstruction -- A Data Symmetry Reduction Technique for Temporal-epistemic Logic -- Tools -- TAPAAL: Editor, Simulator and Verifier of Timed-Arc Petri Nets -- CLAN: A Tool for Contract Analysis and Conflict Discovery -- UnitCheck: Unit Testing and Model Checking Combined -- Probabilistic Systems -- LTL Model Checking of Time-Inhomogeneous Markov Chains -- Statistical Model Checking Using Perfect Simulation -- Quantitative Analysis under Fairness Constraints -- A Decompositional Proof Scheme for Automated Convergence Proofs of Stochastic Hybrid Systems -- Medley -- Memory Usage Verification Using Hip/Sleek -- Solving Parity Games in Practice -- Automated Analysis of Data-Dependent Programs with Dynamic Memory -- Temporal Logic I -- On-the-fly Emptiness Check of Transition-Based Streett Automata -- On Minimal Odd Rankings for Büchi Complementation -- Specification Languages for Stutter-Invariant Regular Properties -- Abstraction and Refinement -- Incremental False Path Elimination for Static Software Analysis -- A Framework for Compositional Verification of Multi-valued Systems via Abstraction-Refinement -- Don’t Know for Multi-valued Systems -- Logahedra: A New Weakly Relational Domain -- Fault Tolerant Systems -- Synthesis of Fault-Tolerant Distributed Systems -- Formal Verification for High-Assurance Behavioral Synthesis -- Dynamic Observers for the Synthesis of Opaque Systems -- Temporal Logic II -- Symbolic CTL Model Checking of Asynchronous Systems Using Constrained Saturation -- LTL Model Checking for Recursive Programs -- On Detecting Regular Predicates in Distributed Systems. |
Altri titoli varianti | ATVA 2009 |
Record Nr. | UNINA-9910484140503321 |
Berlin ; ; Heidelberg, : Springer-Verlag, c2009 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Formal Methods and Hybrid Real-Time Systems [[electronic resource] ] : Essays in Honour of Dines Bjorner and Zhou Chaochen on the Occasion of Their 70th Birthdays / / edited by Cliff B. Jones, Zhiming Liu, Jim Woodcock |
Edizione | [1st ed. 2007.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
Descrizione fisica | 1 online resource (XVI, 542 p.) |
Disciplina | 004.33 |
Collana | Theoretical Computer Science and General Issues |
Soggetto topico |
Software engineering
Computer science Computer engineering Computer networks Machine theory Software Engineering Computer Science Logic and Foundations of Programming Computer Engineering and Networks Formal Languages and Automata Theory |
ISBN | 3-540-75221-8 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Models and Software Model Checking of a Distributed File Replication System -- From “Formal Methods” to System Modeling -- A Denotational Semantics for Handel-C -- Generating Polynomial Invariants with DISCOVERER and QEPCAD -- Harnessing rCOS for Tool Support —The CoCoME Experience -- Automating Verification of Cooperation, Control, and Design in Traffic Applications -- Specifying Various Time Models with Temporal Propositional Variables in Duration Calculus -- Relating Domain Concepts Intensionally by Ordering Connections -- Programmable Messaging for Electronic Government - Building a Foundation -- Balancing Insight and Effort: The Industrial Uptake of Formal Methods -- Proving Theorems About JML Classes -- Specification for Testing -- Semantics and Verification of a Language for Modelling Hardware Architectures -- A Domain-Oriented, Model-Based Approach for Construction and Verification of Railway Control Systems -- Compensable Programs -- Deriving Specifications for Systems That Are Connected to the Physical World -- Engineering the Development of Embedded Systems -- Design Verification Patterns -- On Revival of Algol-Concepts in Modern Programming and Specification Languages -- Design in CommUnity with Extension Morphisms -- Symbolic Test Generation Using a Temporal Logic with Constrained Events -- Expansive-Bisimulation for Context-Free Processes -- VDM Semantics of Programming Languages: Combinators and Monads -- Formal Approach to Railway Applications -- Services as a Paradigm of Computation. |
Record Nr. | UNISA-996465958703316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Formal Methods and Hybrid Real-Time Systems : Essays in Honour of Dines Bjorner and Zhou Chaochen on the Occasion of Their 70th Birthdays / / edited by Cliff B. Jones, Zhiming Liu, Jim Woodcock |
Edizione | [1st ed. 2007.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
Descrizione fisica | 1 online resource (XVI, 542 p.) |
Disciplina | 004.33 |
Collana | Theoretical Computer Science and General Issues |
Soggetto topico |
Software engineering
Computer science Computer engineering Computer networks Machine theory Software Engineering Computer Science Logic and Foundations of Programming Computer Engineering and Networks Formal Languages and Automata Theory |
ISBN | 3-540-75221-8 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Models and Software Model Checking of a Distributed File Replication System -- From “Formal Methods” to System Modeling -- A Denotational Semantics for Handel-C -- Generating Polynomial Invariants with DISCOVERER and QEPCAD -- Harnessing rCOS for Tool Support —The CoCoME Experience -- Automating Verification of Cooperation, Control, and Design in Traffic Applications -- Specifying Various Time Models with Temporal Propositional Variables in Duration Calculus -- Relating Domain Concepts Intensionally by Ordering Connections -- Programmable Messaging for Electronic Government - Building a Foundation -- Balancing Insight and Effort: The Industrial Uptake of Formal Methods -- Proving Theorems About JML Classes -- Specification for Testing -- Semantics and Verification of a Language for Modelling Hardware Architectures -- A Domain-Oriented, Model-Based Approach for Construction and Verification of Railway Control Systems -- Compensable Programs -- Deriving Specifications for Systems That Are Connected to the Physical World -- Engineering the Development of Embedded Systems -- Design Verification Patterns -- On Revival of Algol-Concepts in Modern Programming and Specification Languages -- Design in CommUnity with Extension Morphisms -- Symbolic Test Generation Using a Temporal Logic with Constrained Events -- Expansive-Bisimulation for Context-Free Processes -- VDM Semantics of Programming Languages: Combinators and Monads -- Formal Approach to Railway Applications -- Services as a Paradigm of Computation. |
Record Nr. | UNINA-9910484920003321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Formal methods and software engineering : 8th International Conference on Formal Engineering Methods, ICFEM 2006, Macao, China, November 1-3, 2006 : proceedings / / Zhiming Liu, Jifeng He (eds.) |
Edizione | [1st ed. 2006.] |
Pubbl/distr/stampa | Berlin ; ; New York, : Springer, c2006 |
Descrizione fisica | 1 online resource (XII, 792 p.) |
Disciplina | 005.13/1 |
Altri autori (Persone) |
LiuZhiming <1961->
HeJifeng <1943-> |
Collana |
Lecture notes in computer science
LNCS sublibrary. SL 2, Programming and software engineering |
Soggetto topico |
Formal methods (Computer science)
Software engineering |
ISBN | 3-540-47462-5 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Keynote Talks -- Program Verification Through Computer Algebra -- JML’s Rich, Inherited Specifications for Behavioral Subtypes -- Three Perspectives in Formal Engineering -- Specification and Verification -- A Method for Formalizing, Analyzing, and Verifying Secure User Interfaces -- Applying Timed Interval Calculus to Simulink Diagrams -- Reducing Model Checking of the Few to the One -- Induction-Guided Falsification -- Verifying ? Models of Industrial Systems with Spin -- Stateful Dynamic Partial-Order Reduction -- Internetware and Web-Based Systems -- User-Defined Atomicity Constraint: A More Flexible Transaction Model for Reliable Service Composition -- Environment Ontology-Based Capability Specification for Web Service Discovery -- Scenario-Based Component Behavior Derivation -- Verification of Computation Orchestration Via Timed Automata -- Towards the Semantics for Web Service Choreography Description Language -- Type Checking Choreography Description Language -- Concurrent, Communicating, Timing and Probabilistic Systems -- Formalising Progress Properties of Non-blocking Programs -- Towards a Fully Generic Theory of Data -- Verifying Statemate Statecharts Using CSP and FDR -- A Reasoning Method for Timed CSP Based on Constraint Solving -- Mapping RT-LOTOS Specifications into Time Petri Nets -- Reasoning Algebraically About Probabilistic Loops -- Object and Component Orientation -- Formal Verification of the Heap Manager of an Operating System Using Separation Logic -- A Statically Verifiable Programming Model for Concurrent Object-Oriented Programs -- Model Checking Dynamic UML Consistency -- Testing and Model Checking -- Conditions for Avoiding Controllability Problems in Distributed Testing -- Generating Test Cases for Constraint Automata by Genetic Symbiosis Algorithm -- Checking the Conformance of Java Classes Against Algebraic Specifications -- Incremental Slicing -- Assume-Guarantee Software Verification Based on Game Semantics -- Optimized Execution of Deterministic Blocks in Java PathFinder -- Tools -- A Tool for a Formal Pattern Modeling Language -- An Open Extensible Tool Environment for Event-B -- Tool for Translating Simulink Models into Input Language of a Model Checker -- Fault-Tolerance and Security -- Verifying Abstract Information Flow Properties in Fault Tolerant Security Devices -- A Language for Modeling Network Availability -- Multi-process Systems Analysis Using Event B: Application to Group Communication Systems -- Specification and Refinement -- Issues in Implementing a Model Checker for Z -- Taking Our Own Medicine: Applying the Refinement Calculus to State-Rich Refinement Model Checking -- Discovering Likely Method Specifications -- Time Aware Modelling and Analysis of Multiclocked VLSI Systems -- SALT—Structured Assertion Language for Temporal Logic. |
Altri titoli varianti |
8th International Conference on Formal Engineering Methods
Eighth International Conference on Formal Engineering Methods International Conference on Formal Engineering Methods ICFEM 2006 |
Record Nr. | UNINA-9910483415603321 |
Berlin ; ; New York, : Springer, c2006 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Mathematical frameworks for component software [[electronic resource] ] : models for analysis and synthesis / / [edited by] Zhiming Liu, He Jifeng |
Pubbl/distr/stampa | Hackensack, NJ, : World Scientific, c2006 |
Descrizione fisica | 1 online resource (368 p.) |
Disciplina | 005.3 |
Altri autori (Persone) |
HeJifeng <1943->
LiuZhiming <1961-> |
Collana | Series on component-based software development |
Soggetto topico |
Component software - Mathematical models
Computer software |
Soggetto genere / forma | Electronic books. |
ISBN |
1-281-37322-2
9786611373221 981-277-283-9 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto |
Contents ; Preface ; 1. Temporal Specification of Component Based Systems with Polymorphic Dynamic Reconfiguration ; 1.1. Introduction ; 1.2. A Model of Reconfigurable Component Based Systems ; 1.3. A Temporal Specification Language ; 1.4. Conclusions ; Bibliography
2. Coordinated Composition of Software Components 2.1. Introduction ; 2.2. Components and Their Composition ; 2.3. System Composition Example ; 2.4. Constraint Automata ; 2.5. ABT as Relations on Timed Data Streams ; 2.6. Reo ; 2.7. Time/Temperature Display Coordinator 2.8. Conclusions Bibliography ; 3. On the Semantics of Componentware: A Coalgebraic Persecutive ; 3.1. Introduction ; 3.2. Why Coalgebra Matters ; 3.3. Components as Coalgebras and their Calculi ; 3.4. Application to the Semantics of UML 3.5. Application to the Design of Component Repositories 3.6. Conclusions and Further Work ; Bibliography ; 4. A Theory for Requirements Specification and Architecture Design of Multi-Functional Software Systems ; 4.1. Motivation ; 4.2. Components Interfaces and Services 4.3. Specifying Structuring Relating and Combining Services 4.4. Architectures: Composing Components and Services ; 4.5. Summary and Outlook ; Bibliography ; 5. Component: From Mobile to Channels ; 5.1. Introduction ; 5.2. UML ; 5.3. The component model 5.4. Inter-component coordination via mobile channels |
Record Nr. | UNINA-9910451534103321 |
Hackensack, NJ, : World Scientific, c2006 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Mathematical frameworks for component software [[electronic resource] ] : models for analysis and synthesis / / [edited by] Zhiming Liu, He Jifeng |
Pubbl/distr/stampa | Hackensack, NJ, : World Scientific, c2006 |
Descrizione fisica | 1 online resource (368 p.) |
Disciplina | 005.3 |
Altri autori (Persone) |
HeJifeng <1943->
LiuZhiming <1961-> |
Collana | Series on component-based software development |
Soggetto topico |
Component software - Mathematical models
Computer software |
ISBN |
1-281-37322-2
9786611373221 981-277-283-9 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto |
Contents ; Preface ; 1. Temporal Specification of Component Based Systems with Polymorphic Dynamic Reconfiguration ; 1.1. Introduction ; 1.2. A Model of Reconfigurable Component Based Systems ; 1.3. A Temporal Specification Language ; 1.4. Conclusions ; Bibliography
2. Coordinated Composition of Software Components 2.1. Introduction ; 2.2. Components and Their Composition ; 2.3. System Composition Example ; 2.4. Constraint Automata ; 2.5. ABT as Relations on Timed Data Streams ; 2.6. Reo ; 2.7. Time/Temperature Display Coordinator 2.8. Conclusions Bibliography ; 3. On the Semantics of Componentware: A Coalgebraic Persecutive ; 3.1. Introduction ; 3.2. Why Coalgebra Matters ; 3.3. Components as Coalgebras and their Calculi ; 3.4. Application to the Semantics of UML 3.5. Application to the Design of Component Repositories 3.6. Conclusions and Further Work ; Bibliography ; 4. A Theory for Requirements Specification and Architecture Design of Multi-Functional Software Systems ; 4.1. Motivation ; 4.2. Components Interfaces and Services 4.3. Specifying Structuring Relating and Combining Services 4.4. Architectures: Composing Components and Services ; 4.5. Summary and Outlook ; Bibliography ; 5. Component: From Mobile to Channels ; 5.1. Introduction ; 5.2. UML ; 5.3. The component model 5.4. Inter-component coordination via mobile channels |
Record Nr. | UNINA-9910777496303321 |
Hackensack, NJ, : World Scientific, c2006 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Mathematical frameworks for component software : models for analysis and synthesis / / [edited by] Zhiming Liu, He Jifeng |
Edizione | [1st ed.] |
Pubbl/distr/stampa | Hackensack, NJ, : World Scientific, c2006 |
Descrizione fisica | 1 online resource (368 p.) |
Disciplina | 005.3 |
Altri autori (Persone) |
HeJifeng <1943->
LiuZhiming <1961-> |
Collana | Series on component-based software development |
Soggetto topico |
Component software - Mathematical models
Computer software |
ISBN |
1-281-37322-2
9786611373221 981-277-283-9 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto |
Contents ; Preface ; 1. Temporal Specification of Component Based Systems with Polymorphic Dynamic Reconfiguration ; 1.1. Introduction ; 1.2. A Model of Reconfigurable Component Based Systems ; 1.3. A Temporal Specification Language ; 1.4. Conclusions ; Bibliography
2. Coordinated Composition of Software Components 2.1. Introduction ; 2.2. Components and Their Composition ; 2.3. System Composition Example ; 2.4. Constraint Automata ; 2.5. ABT as Relations on Timed Data Streams ; 2.6. Reo ; 2.7. Time/Temperature Display Coordinator 2.8. Conclusions Bibliography ; 3. On the Semantics of Componentware: A Coalgebraic Persecutive ; 3.1. Introduction ; 3.2. Why Coalgebra Matters ; 3.3. Components as Coalgebras and their Calculi ; 3.4. Application to the Semantics of UML 3.5. Application to the Design of Component Repositories 3.6. Conclusions and Further Work ; Bibliography ; 4. A Theory for Requirements Specification and Architecture Design of Multi-Functional Software Systems ; 4.1. Motivation ; 4.2. Components Interfaces and Services 4.3. Specifying Structuring Relating and Combining Services 4.4. Architectures: Composing Components and Services ; 4.5. Summary and Outlook ; Bibliography ; 5. Component: From Mobile to Channels ; 5.1. Introduction ; 5.2. UML ; 5.3. The component model 5.4. Inter-component coordination via mobile channels |
Record Nr. | UNINA-9910820226703321 |
Hackensack, NJ, : World Scientific, c2006 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Theoretical aspects of computing : ICTAC 2004 : first international colloquium, Guiyang, China, September 20-24, 2004 : revised selected papers / / Zhiming Liu, Keijiro Araki (eds.) |
Edizione | [1st ed. 2005.] |
Pubbl/distr/stampa | Berlin ; ; New York, : Springer, c2005 |
Descrizione fisica | 1 online resource (XIV, 566 p.) |
Disciplina | 004 |
Altri autori (Persone) |
LiuZhiming <1961->
ArakiKeijiro <1954-> |
Collana | Lecture notes in computer science |
Soggetto topico |
Electronic data processing
Information theory |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Speakers -- Software Services: Scientific Challenge or Industrial Hype? -- Integrating Variants of DC -- Challenges in Increasing Tool Support for Programming -- A Predicate Spatial Logic and Model Checking for Mobile Processes -- Concurrent and Distributed Systems -- Object Connectivity and Full Abstraction for a Concurrent Calculus of Classes -- Specifying Software Connectors -- Replicative – Distribution Rules in P Systems with Active Membranes -- A Generalisation of a Relational Structures Model of Concurrency -- A Logical Characterization of Efficiency Preorders -- Inherent Causal Orderings of Partial Order Scenarios -- Atomic Components -- Towards an Optimization-Based Method for Consolidating Domain Variabilities in Domain-Specific Web Services Composition -- Model Integration and Theory Unification -- A Formal Framework for Ontology Integration Based on a Default Extension to DDL -- A Predicative Semantic Model for Integrating UML Models -- An Automatic Mapping from Statecharts to Verilog -- Reverse Observation Equivalence Between Labelled State Transition Systems -- Program Reasoning and Testing -- Minimal Spanning Set for Coverage Testing of Interactive Systems -- An Approach to Integration Testing Based on Data Flow Specifications -- Combining Algebraic and Model-Based Test Case Generation -- Verifying OWL and ORL Ontologies in PVS -- Verification -- Symbolic and Parametric Model Checking of Discrete-Time Markov Chains -- Verifying Linear Duration Constraints of Timed Automata -- Idempotent Relations in Isabelle/HOL -- Program Verification Using Automatic Generation of Invariants, -- Theories of Programming and Programming Languages -- Random Generators for Dependent Types -- A Proof of Weak Termination Providing the Right Way to Terminate -- Nelson-Oppen, Shostak and the Extended Canonizer: A Family Picture with a Newborn -- Real Time Reactive Programming in Lucid Enriched with Contexts -- Revision Programs with Explicit Negation -- Real-Time and Co-design -- An Algebraic Approach for Codesign -- Duration Calculus: A Real-Time Semantic for B -- An Algebra of Petri Nets with Arc-Based Time Restrictions -- A Calculus for Shapes in Time and Space -- A Framework for Specification and Validation of Real-Time Systems Using Circus Actions -- Automata Theory and Logics -- Switched Probabilistic I/O Automata -- Decomposing Controllers into Non-conflicting Distributed Controllers -- Reasoning About Co–Büchi Tree Automata -- Foundations for the Run-Time Monitoring of Reactive Systems – Fundamentals of the MaC Language -- Tutorials at ICTAC 2004 -- A Summary of the Tutorials at ICTAC 2004. |
Altri titoli varianti | ICTAC 2004 |
Record Nr. | UNINA-9910484087203321 |
Berlin ; ; New York, : Springer, c2005 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
Theoretical Aspects of Computing - ICTAC 2007 [[electronic resource] ] : 4th International Colloquium, Macau, China, September 26-28, 2007, Proceedings / / edited by Cliff B. Jones, Zhiming Liu, Jones Woodcock |
Edizione | [1st ed. 2007.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
Descrizione fisica | 1 online resource (XI, 486 p.) |
Disciplina | 004 |
Collana | Theoretical Computer Science and General Issues |
Soggetto topico |
Computer science
Machine theory Compilers (Computer programs) Software engineering Theory of Computation Computer Science Logic and Foundations of Programming Formal Languages and Automata Theory Compilers and Interpreters Software Engineering |
ISBN | 3-540-75292-7 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Domain Theory: Practice and Theories A Discussion of Possible Research Topics -- Linking Semantic Models -- Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems -- Mobile Ambients with Timers and Types -- Automatic Refinement of Split Binary Semaphore -- Stepwise Development of Simulink Models Using the Refinement Calculus Framework -- Bisimulations for a Distributed Higher Order ?-Calculus -- A Complete and Compact Propositional Deontic Logic -- Verifying Lock-Freedom Using Well-Founded Orders -- Tree Components Programming: An Application to XML -- A Framework for Incorporating Trust into Formal Systems Development -- A Higher-Order Demand-Driven Narrowing Calculus with Definitional Trees -- Distributed Time-Asynchronous Automata -- Skolem Machines and Geometric Logic -- A Logical Calculus for Modelling Interferences -- Reflection and Preservation of Properties in Coalgebraic (bi)Simulations -- Controlling Process Modularity in Mobile Computing -- Failures: Their Definition, Modelling and Analysis -- C WS: A Timed Service-Oriented Calculus -- Regular Linear Temporal Logic -- Algebraic Semantics for Compensable Transactions -- Axiomatizing Extended Temporal Logic Fragments Via Instantiation -- Deciding Weak Bisimilarity of Normed Context-Free Processes Using Tableau -- Linear Context Free Languages -- FM for FMS: Lessons Learned While Applying Formal Methods to the Study of Flexible Manufacturing Systems -- On Equality Predicates in Algebraic Specification Languages -- Data-Distributions in PowerList Theory -- Quasi-interpretation Synthesis by Decomposition -- Composing Transformations to Optimize Linear Code -- Building Extended Canonizers by Graph-Based Deduction -- A Randomized Algorithm for BBCSPs in the Prover-Verifier Model -- On the Expressive Power of QLTL. |
Record Nr. | UNISA-996465286203316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Theoretical Aspects of Computing - ICTAC 2007 : 4th International Colloquium, Macau, China, September 26-28, 2007, Proceedings / / edited by Cliff B. Jones, Zhiming Liu, Jones Woodcock |
Edizione | [1st ed. 2007.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 |
Descrizione fisica | 1 online resource (XI, 486 p.) |
Disciplina | 004 |
Collana | Theoretical Computer Science and General Issues |
Soggetto topico |
Computer science
Machine theory Compilers (Computer programs) Software engineering Theory of Computation Computer Science Logic and Foundations of Programming Formal Languages and Automata Theory Compilers and Interpreters Software Engineering |
ISBN | 3-540-75292-7 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Domain Theory: Practice and Theories A Discussion of Possible Research Topics -- Linking Semantic Models -- Discovering Non-linear Ranking Functions by Solving Semi-algebraic Systems -- Mobile Ambients with Timers and Types -- Automatic Refinement of Split Binary Semaphore -- Stepwise Development of Simulink Models Using the Refinement Calculus Framework -- Bisimulations for a Distributed Higher Order ?-Calculus -- A Complete and Compact Propositional Deontic Logic -- Verifying Lock-Freedom Using Well-Founded Orders -- Tree Components Programming: An Application to XML -- A Framework for Incorporating Trust into Formal Systems Development -- A Higher-Order Demand-Driven Narrowing Calculus with Definitional Trees -- Distributed Time-Asynchronous Automata -- Skolem Machines and Geometric Logic -- A Logical Calculus for Modelling Interferences -- Reflection and Preservation of Properties in Coalgebraic (bi)Simulations -- Controlling Process Modularity in Mobile Computing -- Failures: Their Definition, Modelling and Analysis -- C WS: A Timed Service-Oriented Calculus -- Regular Linear Temporal Logic -- Algebraic Semantics for Compensable Transactions -- Axiomatizing Extended Temporal Logic Fragments Via Instantiation -- Deciding Weak Bisimilarity of Normed Context-Free Processes Using Tableau -- Linear Context Free Languages -- FM for FMS: Lessons Learned While Applying Formal Methods to the Study of Flexible Manufacturing Systems -- On Equality Predicates in Algebraic Specification Languages -- Data-Distributions in PowerList Theory -- Quasi-interpretation Synthesis by Decomposition -- Composing Transformations to Optimize Linear Code -- Building Extended Canonizers by Graph-Based Deduction -- A Randomized Algorithm for BBCSPs in the Prover-Verifier Model -- On the Expressive Power of QLTL. |
Record Nr. | UNINA-9910482956503321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2007 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|