top

  Info

  • Utilizzare la checkbox di selezione a fianco di ciascun documento per attivare le funzionalità di stampa, invio email, download nei formati disponibili del (i) record.

  Info

  • Utilizzare questo link per rimuovere la selezione effettuata.
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
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
Opac: Controlla la disponibilità qui
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
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
Opac: Controlla la disponibilità qui
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
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
Opac: Controlla la disponibilità qui
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
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
Opac: Controlla la disponibilità qui
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
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
Opac: Controlla la disponibilità qui
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
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
Opac: Controlla la disponibilità qui