FME 2003: Formal Methods [[electronic resource] ] : International Symposium of Formal Methods Europe. Pisa Italy, September 8-14, 2003, Proceedings / / edited by Keijiro Araki, Stefania Gnesi, Dion Mandrioli |
Edizione | [1st ed. 2003.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2003 |
Descrizione fisica | 1 online resource (XXXIV, 946 p.) |
Disciplina | 005.1 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Software engineering
Computer logic Computer programming Programming languages (Electronic computers) Mathematical logic Software Engineering/Programming and Operating Systems Logics and Meanings of Programs Programming Techniques Software Engineering Programming Languages, Compilers, Interpreters Mathematical Logic and Formal Languages |
ISBN | 3-540-45236-2 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Speakers -- Looking Back to the Future -- Past, Present, and Future of SRA Implementation of CafeOBJ -- On Failures and Faults -- Trends in Software Verification -- Event Based Sequential Program Development: Application to Constructing a Pointer Program -- I-Day -- Proving the Shalls -- Adaptable Translator of B Specifications to Embedded C Programs -- Integrating Model-Checking Architectural Analysis and Validation in a Real Software Life-Cycle -- Lessons Learned from a Successful Implementation of Formal Methods in an Industrial Project -- Control Systems and Industrial Applications -- Determining the Specification of a Control System from That of Its Environment -- Managerial Issues for the Consideration and Use of Formal Methods -- Verifying Emulation of Legacy Mission Computer Systems -- Improving Safety Assessment of Complex Systems: An Industrial Case Study -- Communications System Verification -- Compositional Verification of an ATM Protocol -- Proving the Correctness of Simpson’s 4-Slot ACM Using an Assertional Rely-Guarantee Proof Method -- Synthesis and Verification of Constraints in the PGM Protocol -- Co-specification and Compilers -- Mapping Statecharts to Verilog for Hardware/Software Co-specification -- A Strategy for Compiling Classes, Inheritance, and Dynamic Binding -- Composition -- A Semantic Foundation for TCOZ in Unifying Theories of Programming -- Refinement and Verification of Synchronized Component-Based Systems -- Certifying and Synthesizing Membership Equational Proofs -- Team Automata Satisfying Compositionality -- Composing Invariants -- Java, Object Orientation and Modularity -- Java Applet Correctness: A Developer-Oriented Approach -- Improving JML: For a Safer and More Effective Language -- Using Abstractions for Heuristic State Space Exploration of Reactive Object-Oriented Systems -- A Formal Framework for Modular Synchronous System Design -- Model Checking -- Generating Counterexamples for Multi-valued Model-Checking -- Combining Real-Time Model-Checking and Fault Tree Analysis -- Model-Checking TRIO Specifications in SPIN -- Computing Meta-transitions for Linear Transition Systems with Polynomials -- Translation-Based Compositional Reasoning for Software Systems -- Watchdog Transformations for Property-Oriented Model-Checking -- Parallel Process -- A Circus Semantics for Ravenscar Protected Objects -- Constructing Deadlock Free Event-Based Applications: A Rely/Guarantee Approach -- A General Approach to Deadlock Freedom Verification for Software Architectures -- Taking Alloy to the Movies -- Interacting State Machines for Mobility -- Composing Temporal-Logic Specifications with Machine Assistance -- Program Checking and Testing -- Model Checking FTA -- Program Checking with Certificates: Separating Correctness-Critical Code -- Reification of Executable Test Scripts in Formal Specification-Based Test Generation: The Java Card Transaction Mechanism Case Study -- Checking and Reasoning about Semantic Web through Alloy -- B Method -- Structuring Retrenchments in B by Decomposition -- Design of an Automatic Prover Dedicated to the Refinement of Database Applications -- ProB: A Model Checker for B -- Security -- SAT-Based Model-Checking of Security Protocols Using Planning Graph Analysis -- Correctness of Source-Level Safety Policies -- A Topological Characterization of TCP/IP Security. |
Record Nr. | UNISA-996465699403316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2003 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
FME 2003: Formal Methods : International Symposium of Formal Methods Europe. Pisa Italy, September 8-14, 2003, Proceedings / / edited by Keijiro Araki, Stefania Gnesi, Dion Mandrioli |
Edizione | [1st ed. 2003.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2003 |
Descrizione fisica | 1 online resource (XXXIV, 946 p.) |
Disciplina | 005.1 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Software engineering
Computer logic Computer programming Programming languages (Electronic computers) Mathematical logic Software Engineering/Programming and Operating Systems Logics and Meanings of Programs Programming Techniques Software Engineering Programming Languages, Compilers, Interpreters Mathematical Logic and Formal Languages |
ISBN | 3-540-45236-2 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | Invited Speakers -- Looking Back to the Future -- Past, Present, and Future of SRA Implementation of CafeOBJ -- On Failures and Faults -- Trends in Software Verification -- Event Based Sequential Program Development: Application to Constructing a Pointer Program -- I-Day -- Proving the Shalls -- Adaptable Translator of B Specifications to Embedded C Programs -- Integrating Model-Checking Architectural Analysis and Validation in a Real Software Life-Cycle -- Lessons Learned from a Successful Implementation of Formal Methods in an Industrial Project -- Control Systems and Industrial Applications -- Determining the Specification of a Control System from That of Its Environment -- Managerial Issues for the Consideration and Use of Formal Methods -- Verifying Emulation of Legacy Mission Computer Systems -- Improving Safety Assessment of Complex Systems: An Industrial Case Study -- Communications System Verification -- Compositional Verification of an ATM Protocol -- Proving the Correctness of Simpson’s 4-Slot ACM Using an Assertional Rely-Guarantee Proof Method -- Synthesis and Verification of Constraints in the PGM Protocol -- Co-specification and Compilers -- Mapping Statecharts to Verilog for Hardware/Software Co-specification -- A Strategy for Compiling Classes, Inheritance, and Dynamic Binding -- Composition -- A Semantic Foundation for TCOZ in Unifying Theories of Programming -- Refinement and Verification of Synchronized Component-Based Systems -- Certifying and Synthesizing Membership Equational Proofs -- Team Automata Satisfying Compositionality -- Composing Invariants -- Java, Object Orientation and Modularity -- Java Applet Correctness: A Developer-Oriented Approach -- Improving JML: For a Safer and More Effective Language -- Using Abstractions for Heuristic State Space Exploration of Reactive Object-Oriented Systems -- A Formal Framework for Modular Synchronous System Design -- Model Checking -- Generating Counterexamples for Multi-valued Model-Checking -- Combining Real-Time Model-Checking and Fault Tree Analysis -- Model-Checking TRIO Specifications in SPIN -- Computing Meta-transitions for Linear Transition Systems with Polynomials -- Translation-Based Compositional Reasoning for Software Systems -- Watchdog Transformations for Property-Oriented Model-Checking -- Parallel Process -- A Circus Semantics for Ravenscar Protected Objects -- Constructing Deadlock Free Event-Based Applications: A Rely/Guarantee Approach -- A General Approach to Deadlock Freedom Verification for Software Architectures -- Taking Alloy to the Movies -- Interacting State Machines for Mobility -- Composing Temporal-Logic Specifications with Machine Assistance -- Program Checking and Testing -- Model Checking FTA -- Program Checking with Certificates: Separating Correctness-Critical Code -- Reification of Executable Test Scripts in Formal Specification-Based Test Generation: The Java Card Transaction Mechanism Case Study -- Checking and Reasoning about Semantic Web through Alloy -- B Method -- Structuring Retrenchments in B by Decomposition -- Design of an Automatic Prover Dedicated to the Refinement of Database Applications -- ProB: A Model Checker for B -- Security -- SAT-Based Model-Checking of Security Protocols Using Planning Graph Analysis -- Correctness of Source-Level Safety Policies -- A Topological Characterization of TCP/IP Security. |
Record Nr. | UNINA-9910767545203321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2003 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
High Performance Computing [[electronic resource] ] : International Symposium, ISHPC'97, Fukuoka, Japan, November 4-6, 1997, Proceedings / / edited by Constantine Polychronopoulos, Kazuki Joe, Keijiro Araki, Makoto Amamiya |
Edizione | [1st ed. 1997.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 |
Descrizione fisica | 1 online resource (XIII, 423 p.) |
Disciplina | 004/.35 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Computers
Software engineering Computer organization Numerical analysis Theory of Computation Software Engineering/Programming and Operating Systems Computer Systems Organization and Communication Networks Numerical Analysis |
ISBN | 3-540-69644-X |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | The generation of optimized codes using nonzero structure analysis -- On the importance of an end-to-end view of memory consistency in future computer systems -- High performance distributed object systems -- Instruction cache prefetching using multilevel branch prediction -- High performance wireless computing -- High-performance computing and applications in image processing and computer vision -- Present and future of HPC technologies -- Evaluation of multithreaded processors and thread-switch policies -- A multithreaded implementation concept of prolog on Datarol-II machine -- Thread Synchronization Unit (TSU): A building block for high performance computers -- Data dependence path reduction with tunneling load instructions -- Performance estimation of embedded software with pipeline and cache hazard modeling -- An implementation and evaluation of a distributed shared-memory system on workstation clusters using fast serial links -- Designing and optimizing 3-connectivity communication networks using a distributed genetic algorithm -- Adaptive routing on the Recursive Diagonal Torus -- Achieving multi-level parallelization -- A technique to eliminate redundant inter-processor communication on parallelizing compiler TINPAR -- An automatic vectorizing/parallelizing Pascal compiler V-Pascal ver. 3 -- An algorithm for automatic detection of loop indices for communication overlapping -- NaraView: An interactive 3D visualization system for parallelization of programs -- Hybrid approach for non-strict dataflow program on commodity machine -- Resource management methods for general purpose massively parallel OS SSS-CORE -- Scenario-based hypersequential programming: Formulation of parallelization -- Parallelization of space plasma particle simulation -- Implementing iterative solvers for irregular sparse matrix problems in high performance Fortran -- Parallel navigation in an A-NETL based parallel OODBMS -- High performance parallel FFT on distributed memory parallel computers -- Parallel computation model logPQ -- Cost estimation of coherence protocols of software managed cache on distributed shared memory system -- A portable distributed shared memory system on the cluster environment: Design and implementation fully in software -- An object-oriented framework for loop parallelization -- A method for runtime recognition of collective communication on distributed-memory multiprocessors -- Improving the performance of automated forward deduction system EnCal -- Efficiency of parallel machine for large-scale simulation in computational physics -- Parallel PDB data retriever “PDB diving booster” -- A parallelization method for neural networks with weak connection design -- Exploiting parallel computers to reduce neural network training time of real applications. |
Record Nr. | UNINA-9910144905403321 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. Federico II | ||
|
High Performance Computing [[electronic resource] ] : International Symposium, ISHPC'97, Fukuoka, Japan, November 4-6, 1997, Proceedings / / edited by Constantine Polychronopoulos, Kazuki Joe, Keijiro Araki, Makoto Amamiya |
Edizione | [1st ed. 1997.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 |
Descrizione fisica | 1 online resource (XIII, 423 p.) |
Disciplina | 004/.35 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Computers
Software engineering Computer organization Numerical analysis Theory of Computation Software Engineering/Programming and Operating Systems Computer Systems Organization and Communication Networks Numerical Analysis |
ISBN | 3-540-69644-X |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | The generation of optimized codes using nonzero structure analysis -- On the importance of an end-to-end view of memory consistency in future computer systems -- High performance distributed object systems -- Instruction cache prefetching using multilevel branch prediction -- High performance wireless computing -- High-performance computing and applications in image processing and computer vision -- Present and future of HPC technologies -- Evaluation of multithreaded processors and thread-switch policies -- A multithreaded implementation concept of prolog on Datarol-II machine -- Thread Synchronization Unit (TSU): A building block for high performance computers -- Data dependence path reduction with tunneling load instructions -- Performance estimation of embedded software with pipeline and cache hazard modeling -- An implementation and evaluation of a distributed shared-memory system on workstation clusters using fast serial links -- Designing and optimizing 3-connectivity communication networks using a distributed genetic algorithm -- Adaptive routing on the Recursive Diagonal Torus -- Achieving multi-level parallelization -- A technique to eliminate redundant inter-processor communication on parallelizing compiler TINPAR -- An automatic vectorizing/parallelizing Pascal compiler V-Pascal ver. 3 -- An algorithm for automatic detection of loop indices for communication overlapping -- NaraView: An interactive 3D visualization system for parallelization of programs -- Hybrid approach for non-strict dataflow program on commodity machine -- Resource management methods for general purpose massively parallel OS SSS-CORE -- Scenario-based hypersequential programming: Formulation of parallelization -- Parallelization of space plasma particle simulation -- Implementing iterative solvers for irregular sparse matrix problems in high performance Fortran -- Parallel navigation in an A-NETL based parallel OODBMS -- High performance parallel FFT on distributed memory parallel computers -- Parallel computation model logPQ -- Cost estimation of coherence protocols of software managed cache on distributed shared memory system -- A portable distributed shared memory system on the cluster environment: Design and implementation fully in software -- An object-oriented framework for loop parallelization -- A method for runtime recognition of collective communication on distributed-memory multiprocessors -- Improving the performance of automated forward deduction system EnCal -- Efficiency of parallel machine for large-scale simulation in computational physics -- Parallel PDB data retriever “PDB diving booster” -- A parallelization method for neural networks with weak connection design -- Exploiting parallel computers to reduce neural network training time of real applications. |
Record Nr. | UNISA-996465562303316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1997 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
RIMS Symposium on Software Science and Engineering II [[electronic resource] ] : Proceedings of the Symposia 1983 and 1984, Kyoto, Japan / / edited by Eiichi Goto, Keijiro Araki, Taiichi Yuasa |
Edizione | [1st ed. 1986.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1986 |
Descrizione fisica | 1 online resource (XIV, 330 p.) |
Disciplina | 005.1 |
Collana | Lecture Notes in Computer Science |
Soggetto topico |
Software engineering
Programming languages (Electronic computers) Computers Software Engineering/Programming and Operating Systems Software Engineering Programming Languages, Compilers, Interpreters Computation by Abstract Devices |
ISBN | 3-540-39809-0 |
Formato | Materiale a stampa |
Livello bibliografico | Monografia |
Lingua di pubblicazione | eng |
Nota di contenuto | A fast parallel merging algorithm for 2–3 trees -- Evaluation of graph representations with active nodes -- On equivalence transformations for term rewriting systems -- A portable logic simulation system for development of FLATS machine -- Partial computation with a dataflow machine -- OR-Parallel Optimizing Prolog System: Pops its design and implementation in Concurrent Prolog -- Incorporating Naïve Negation into Prolog -- Algebraic specification method of programming languages -- Multiversion concurrency control scheme for a distributed database system — A trial to break concurrent update of redundant copies — -- Global storage allocation in attribute evaluation -- On program transformation with tupling technique -- Evaluation of working set algorithms for data-flow machines -- Comparison of closure reduction and combinatory reduction schemes -- The BC-chain method for representing combinators in linear space -- Circuit simulation code generation by computer algebra -- List 1 Algebraic code for simple harmonic motion -- List 2 Generated fortran code for simple harmonic motion. |
Record Nr. | UNISA-996465706603316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 1986 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|
Theoretical Aspects of Computing - ICTAC 2004 [[electronic resource] ] : First International Colloquium Guiyand, China, September 20-24, 2004, Revised Selected Papers / / edited by Zhiming Liu, Keijiro Araki |
Edizione | [1st ed. 2005.] |
Pubbl/distr/stampa | Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 |
Descrizione fisica | 1 online resource (XIV, 566 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 |
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. |
Record Nr. | UNISA-996465706903316 |
Berlin, Heidelberg : , : Springer Berlin Heidelberg : , : Imprint : Springer, , 2005 | ||
Materiale a stampa | ||
Lo trovi qui: Univ. di Salerno | ||
|