ALBERT

All Library Books, journals and Electronic Records Telegrafenberg

feed icon rss

Your email was sent successfully. Check your inbox.

An error occurred while sending the email. Please try again.

Proceed reservation?

Export
Filter
  • (α-Aminoalkyl)phosphonic acids
  • Aluminum
  • Computer Programming and Software
Collection
Keywords
Publisher
  • 1
    Electronic Resource
    Electronic Resource
    Springer
    Journal of chemical crystallography 30 (2000), S. 219-222 
    ISSN: 1572-8854
    Keywords: Aluminum ; alkoxide ; five-coordinate ; six-coordinate
    Source: Springer Online Journal Archives 1860-2000
    Topics: Geosciences , Physics
    Notes: Abstract The present contribution will demonstrate that monomeric alkoxide compounds can be formed by the use of the Salen(tBu) ligand. These alkoxides, LAlOR (with L=Salen (tBu), R=Me (1), Salomphen(tBu), R=Me (3) and L=Salen(tBu), R=Et (4)) feature five-coordinate monomeric aluminum (Salen(tBu)=N,N′-ethylenebis(3,5-di-tert-butylsalicylideneimine) and Salomphen(tBu)=N,N′-(4,5-di-methyl)phenylenenebis(3,5-di-tert-butylsalicylideneimine). Crystallization of 1 from MeOH affords the six-coordinate complex, Salen(tBu)AlOMe(MeOH) (2). The manner in which these compounds may be obtained, as well as the structures of 2 and 4 will be described
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 2
    Electronic Resource
    Electronic Resource
    Springer
    Journal of chemical crystallography 30 (2000), S. 215-218 
    ISSN: 1572-8854
    Keywords: Aluminum ; cation ; Lewis acid ; six-coordinate
    Source: Springer Online Journal Archives 1860-2000
    Topics: Geosciences , Physics
    Notes: Abstract The chiral five-coordinate halide compound, Salcen(tBu)AlCl (1) (Salcen = N,N′-cyclohexylenebis(3, 5-di-tert-butylsalicylideneimine) can be used in a salt elimination reaction to produce [R,R'Salcen(tBu)AlOTs] (2) as well as the chiral cationic complex, [R,R'Salcen (tBu)Al(thf)2]+ BPh4 − (3). The conditions under which these types of neutral and cationic complexes form will be discussed. This should provide guidance for the eventual use of the cations as strongly Lewis acidic catalysts and organic synthetic reagents.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 3
    Electronic Resource
    Electronic Resource
    Amsterdam : Elsevier
    Environmental and Experimental Botany 34 (1994), S. 329-336 
    ISSN: 0098-8472
    Keywords: Aluminum ; fosetyl-Al ; grapevine (Vitis vinifera cv. Monastrell) ; peroxidase secretion ; resveratrol ; suspension cell cultures
    Source: Elsevier Journal Backfiles on ScienceDirect 1907 - 2002
    Topics: Biology
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 4
    Electronic Resource
    Electronic Resource
    Weinheim : Wiley-Blackwell
    Liebigs Annalen 2000 (2000), S. 281-289 
    ISSN: 1434-193X
    Keywords: Phosphorus acid amphiphiles ; (α-Aminoalkyl)phosphonic acids ; Carboxyalkyl (α-aminoalkyl)phosphonic acid monoesters ; Spiro compounds ; Pudovik reaction ; Chemistry ; General Chemistry
    Source: Wiley InterScience Backfile Collection 1832-2000
    Topics: Chemistry and Pharmacology
    Notes: ---The addition reaction between the P-H bond of tetraoxyspirophosphoranes 1-2 and long-chain imines 3a-h (decyl, dodecyl, tetradecyl, hexadecyl, octadecyl, and oleyl imines) occurs instantaneously at room temperature. It is diastereoselective, and quantitatively leads to the corresponding (α-aminoalkyl)spirophosphoranes 4a-h and 5e. The influence of the pentacoordinated phosphorus atom on the stereoselectivity of the Pudovik reaction might be attributed to the involvement of the rigid spirophosphoranide (PV) intermediate in the addition reaction. Selective and one-pot hydrolysis of these P-C bond spirophosphoranes readily proceeds either at room temperature in the presence of moist solvents to give the corresponding carboxyalkyl (α-aminoalkyl)phosphonic acid monoesters 6a-h and 7e, or the reaction may be carried out in the presence of 20% aqueous hydrochloric acid under reflux, to afford the free (α-aminoalkyl)phosphonic acid amphiphiles 8a-h in high yields. In contrast to their sodium salts, these single- and double-chained free and monoester phosphonic acid amphiphiles exist as zwitterions and are not soluble in water.
    Additional Material: 2 Tab.
    Type of Medium: Electronic Resource
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 5
    Publication Date: 2018-06-11
    Description: This tutorial provides an overview of the PVS strategy language, and explains how to define new PVS strategies and load them into PVS, and how to create a strategy package. It then discusses several useful techniques that can be used in developing user strategies, and provides examples that illustrate many of these techniques.
    Keywords: Computer Programming and Software
    Type: Design and Application of Strategies/Tactics in Higher Order Logics; 16-42; NASA/CP-2003-212448
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 6
    Publication Date: 2019-07-27
    Description: This paper presents a mathematical foundation and a rewriting logic infrastructure for the execution and property veri cation of synchronous set relations. The mathematical foundation is given in the language of abstract set relations. The infrastructure consists of an ordersorted rewrite theory in Maude, a rewriting logic system, that enables the synchronous execution of a set relation provided by the user. By using the infrastructure, existing algorithm veri cation techniques already available in Maude for traditional asynchronous rewriting, such as reachability analysis and model checking, are automatically available to synchronous set rewriting. The use of the infrastructure is illustrated with an executable operational semantics of a simple synchronous language and the veri cation of temporal properties of a synchronous system.
    Keywords: Computer Programming and Software
    Type: NF1676L-12963 , Brazilian Symposium on Formal Methods; 26-30 Sept. 2011; Sao Paulo; Brazil
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 7
    Publication Date: 2019-07-13
    Description: This paper explores a new approach to validating software implementations that have been produced from formally-verified algorithms. Although visual inspection gives some confidence that the implementations faithfully reflect the formal models, it does not provide complete assurance that the software is correct. The proposed approach, which is based on animation of formal specifications, compares the outputs computed by the software implementations on a given suite of input values to the outputs computed by the formal models on the same inputs, and determines if they are equal up to a given tolerance. The approach is illustrated on a prototype air traffic management system that computes simple kinematic trajectories for aircraft. Proofs for the mathematical models of the system's algorithms are carried out in the Prototype Verification System (PVS). The animation tool PVSio is used to evaluate the formal models on a set of randomly generated test cases. Output values computed by PVSio are compared against output values computed by the actual software. This comparison improves the assurance that the translation from formal models to code is faithful and that, for example, floating point errors do not greatly affect correctness and safety properties.
    Keywords: Computer Programming and Software
    Type: NF1676L-20845 , International Conference on Tests & Proofs (TAP 2015); Jul 22, 2015 - Jul 24, 2015; L''Aquila; Italy
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 8
    Publication Date: 2019-07-12
    Description: As the technological and operational capabilities of unmanned aircraft systems (UAS) have grown, so too have international efforts to integrate UAS into civil airspace. However, one of the major concerns that must be addressed in realizing this integration is that of safety. For example, UAS lack an on-board pilot to comply with the legal requirement that pilots see and avoid other aircraft. This requirement has motivated the development of a detect and avoid (DAA) capability for UAS that provides situational awareness and maneuver guidance to UAS operators to aid them in avoiding and remaining well clear of other aircraft in the airspace. The NASA Langley Research Center Formal Methods group has played a fundamental role in the development of this capability. This article gives a selected survey of the formal methods work conducted in support of the development of a DAA concept for UAS. This work includes specification of low-level and high-level functional requirements, formal verification of algorithms, and rigorous validation of software implementations.
    Keywords: Computer Programming and Software
    Type: NF1676L-24045
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 9
    facet.materialart.
    Unknown
    In:  CASI
    Publication Date: 2019-07-12
    Description: Combining symbolic techniques such as: (i) SMT solving, (ii) rewriting modulo theories, and (iii) model checking can enable the analysis of infinite-state systems outside the scope of each such technique. This paper proposes rewriting modulo SMT as a new technique combining the powers of (i)-(iii) and ideally suited to model and analyze infinite-state open systems; that is, systems that interact with a non-deterministic environment. Such systems exhibit both internal non-determinism due to the system, and external non-determinism due to the environment. They are not amenable to finite-state model checking analysis because they typically are infinite-state. By being reducible to standard rewriting using reflective techniques, rewriting modulo SMT can both naturally model and analyze open systems without requiring any changes to rewriting-based reachability analysis techniques for closed systems. This is illustrated by the analysis of a real-time system beyond the scope of timed automata methods.
    Keywords: Computer Programming and Software
    Type: NASA/TM-2013-218033 , L-20315 , NF1676L-17235
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
  • 10
    Publication Date: 2019-07-12
    Description: Declarative specifications of digital systems often contain parts that can be automatically translated into executable code. Automated code generation may reduce or eliminate the kinds of errors typically introduced through manual code writing. For this approach to be effective, the generated code should be reasonably efficient and, more importantly, verifiable. This paper presents a prototype code generator for the Prototype Verification System (PVS) that translates a subset of PVS functional specifications into an intermediate language and subsequently to multiple target programming languages. Several case studies are presented to illustrate the tool's functionality. The generated code can be analyzed by software verification tools such as verification condition generators, static analyzers, and software model-checkers to increase the confidence that the generated code is correct.
    Keywords: Computer Programming and Software
    Type: NASA/TM-2009-215943 , L-19766 , LF99-9439
    Format: application/pdf
    Location Call Number Expected Availability
    BibTip Others were also interested in ...
Close ⊗
This website uses cookies and the analysis tool Matomo. More information can be found here...