| 1. |
- Blanton, Michael R., et al.
(författare)
-
Sloan Digital Sky Survey IV : Mapping the Milky Way, Nearby Galaxies, and the Distant Universe
- 2017
-
Ingår i: Astronomical Journal. - : IOP Publishing Ltd. - 0004-6256 .- 1538-3881. ; 154:1
-
Tidskriftsartikel (refereegranskat)abstract
- We describe the Sloan Digital Sky Survey IV (SDSS-IV), a project encompassing three major spectroscopic programs. The Apache Point Observatory Galactic Evolution Experiment 2 (APOGEE-2) is observing hundreds of thousands of Milky Way stars at high resolution and. high signal-to-noise ratios in the near-infrared. The Mapping Nearby Galaxies at Apache Point Observatory (MaNGA) survey is obtaining spatially resolved spectroscopy for thousands of nearby galaxies (median z similar to 0.03). The extended Baryon Oscillation Spectroscopic Survey (eBOSS) is mapping the galaxy, quasar, and neutral gas distributions between z similar to 0.6 and 3.5 to constrain cosmology using baryon acoustic oscillations, redshift space distortions, and the shape of the power spectrum. Within eBOSS, we are conducting two major subprograms: the SPectroscopic IDentification of eROSITA Sources (SPIDERS), investigating X-ray AGNs. and galaxies in X-ray clusters, and the Time Domain Spectroscopic Survey (TDSS), obtaining spectra of variable sources. All programs use the 2.5 m Sloan Foundation Telescope at the. Apache Point Observatory; observations there began in Summer 2014. APOGEE-2 also operates a second near-infrared spectrograph at the 2.5 m du Pont Telescope at Las Campanas Observatory, with observations beginning in early 2017. Observations at both facilities are scheduled to continue through 2020. In keeping with previous SDSS policy, SDSS-IV provides regularly scheduled public data releases; the first one, Data Release 13, was made available in 2016 July.
|
|
| 2. |
- Abolfathi, Bela, et al.
(författare)
-
The Fourteenth Data Release of the Sloan Digital Sky Survey : First Spectroscopic Data from the Extended Baryon Oscillation Spectroscopic Survey and from the Second Phase of the Apache Point Observatory Galactic Evolution Experiment
- 2018
-
Ingår i: Astrophysical Journal Supplement Series. - : IOP Publishing Ltd. - 0067-0049 .- 1538-4365. ; 235:2
-
Tidskriftsartikel (refereegranskat)abstract
- The fourth generation of the Sloan Digital Sky Survey (SDSS-IV) has been in operation since 2014 July. This paper describes the second data release from this phase, and the 14th from SDSS overall (making this Data Release Fourteen or DR14). This release makes the data taken by SDSS-IV in its first two years of operation (2014-2016 July) public. Like all previous SDSS releases, DR14 is cumulative, including the most recent reductions and calibrations of all data taken by SDSS since the first phase began operations in 2000. New in DR14 is the first public release of data from the extended Baryon Oscillation Spectroscopic Survey; the first data from the second phase of the Apache Point Observatory (APO) Galactic Evolution Experiment (APOGEE-2), including stellar parameter estimates from an innovative data-driven machine-learning algorithm known as "The Cannon"; and almost twice as many data cubes from the Mapping Nearby Galaxies at APO (MaNGA) survey as were in the previous release (N = 2812 in total). This paper describes the location and format of the publicly available data from the SDSS-IV surveys. We provide references to the important technical papers describing how these data have been taken (both targeting and observation details) and processed for scientific use. The SDSS web site (www.sdss.org) has been updated for this release and provides links to data downloads, as well as tutorials and examples of data use. SDSS-IV is planning to continue to collect astronomical data until 2020 and will be followed by SDSS-V.
|
|
| 3. |
- Aguado, D. S., et al.
(författare)
-
The Fifteenth Data Release of the Sloan Digital Sky Surveys : First Release of MaNGA-derived Quantities, Data Visualization Tools, and Stellar Library
- 2019
-
Ingår i: Astrophysical Journal Supplement Series. - : Institute of Physics Publishing (IOPP). - 0067-0049 .- 1538-4365. ; 240:2
-
Tidskriftsartikel (refereegranskat)abstract
- Twenty years have passed since first light for the Sloan Digital Sky Survey (SDSS). Here, we release data taken by the fourth phase of SDSS (SDSS-IV) across its first three years of operation (2014 July-2017 July). This is the third data release for SDSS-IV, and the 15th from SDSS (Data Release Fifteen; DR15). New data come from MaNGA-we release 4824 data cubes, as well as the first stellar spectra in the MaNGA Stellar Library (MaStar), the first set of survey-supported analysis products (e.g., stellar and gas kinematics, emission-line and other maps) from the MaNGA Data Analysis Pipeline, and a new data visualization and access tool we call "Marvin." The next data release, DR16, will include new data from both APOGEE-2 and eBOSS; those surveys release no new data here, but we document updates and corrections to their data processing pipelines. The release is cumulative; it also includes the most recent reductions and calibrations of all data taken by SDSS since first light. In this paper, we describe the location and format of the data and tools and cite technical references describing how it was obtained and processed. The SDSS website (www.sdss.org) has also been updated, providing links to data downloads, tutorials, and examples of data use. Although SDSS-IV will continue to collect astronomical data until 2020, and will be followed by SDSS-V (2020-2025), we end this paper by describing plans to ensure the sustainability of the SDSS data archive for many years beyond the collection of data.
|
|
| 4. |
- Sanchez Perez, Cesar, 1981, et al.
(författare)
-
A survey of challenges for runtime verification from advanced application domains (beyond software)
- 2019
-
Ingår i: Formal Methods in System Design. - : Springer Science and Business Media LLC. - 1572-8102 .- 0925-9856. ; 54:3, s. 279-335
-
Tidskriftsartikel (refereegranskat)abstract
- Runtime verification is an area of formal methods that studies the dynamic analysis of execution traces against formal specifications. Typically, the two main activities in runtime verification efforts are the process of creating monitors from specifications, and the algorithms for the evaluation of traces against the generated monitors. Other activities involve the instrumentation of the system to generate the trace and the communication between the system under analysis and the monitor. Most of the applications in runtime verification have been focused on the dynamic analysis of software, even though there are many more potential applications to other computational devices and target systems. In this paper we present a collection of challenges for runtime verification extracted from concrete application domains, focusing on the difficulties that must be overcome to tackle these specific challenges. The computational models that characterize these domains require to devise new techniques beyond the current state of the art in runtime verification.
|
|
| 5. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
A Unified Approach for Static and Runtime Verification: Framework and Applications
- 2012
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Berlin, Heidelberg : Springer Berlin Heidelberg. - 1611-3349 .- 0302-9743. - 9783642340253 ; :PART 1, s. 312-326
-
Konferensbidrag (refereegranskat)abstract
- Static verification of software is becoming ever more effective and efficient. Still, static techniques either have high precision, in which case powerful judgements are hard to achieve automatically, or they use abstractions supporting increased automation, but possibly losing important aspects of the concrete system in the process. Runtime verification has complementary strengths and weaknesses. It combines full precision of the model (including the real deployment environment) with full automation, but cannot judge future and alternative runs. Another drawback of runtime verification can be the computational overhead of monitoring the running system which, although typically not very high, can still be prohibitive in certain settings. In this paper, we propose a framework to combine static analysis techniques and runtime verification with the aim of getting the best of both techniques. In particular, we discuss an instantiation of our framework for the deductive theorem prover KeY, and the runtime verification tool LARVA. Apart from combining static and dynamic verification, this approach also combines the data centric analysis of KeY with the control centric analysis of LARVA. An advantage of the approach is that, through the use of a single specification which can be used by both analysis techniques, expensive parts of the analysis could be moved to the static phase, allowing the runtime monitor to make significant assumptions, dropping parts of expensive checks at runtime. We also discuss specific applications of our approach.
|
|
| 6. |
- Ahrendt, Wolfgang, 1967, et al.
(författare)
-
StaRVOOrS - Episode II: Strengthen and distribute the force
- 2016
-
Ingår i: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). - Cham : Springer International Publishing. - 1611-3349 .- 0302-9743. - 9783319471655 ; 9952, s. 402-415
-
Konferensbidrag (refereegranskat)abstract
- Static and runtime techniques for the verification of programs are complementary. They both have their advantages and disadvantages, and a natural question is whether they may be combined in such a way as to get the advantages of both without inheriting too much from their disadvantages. In a previous contribution to ISoLA’12, we have proposed StaRVOOrS (‘Static and Runtime Verification of Object- Oriented Software’), a unified framework for combining static and runtime verification in order to check data- and control-oriented properties. Returning to ISoLA here, we briefly report on advances since then: a unified specification language for data- and control-oriented properties, a tool for combined static and runtime verification, and experiments. On that basis, we discuss two future research directions to strengthen the power, and broaden the scope, of combined static and runtime verification: (i) to use static analysis techniques to further optimise the runtime monitor, and (ii) to extend the framework to the distributed case.
|
|
| 7. |
- Azzopardi, Shaun, 1992, et al.
(författare)
-
AspectSol: A Solidity Aspect-Oriented Programming Tool with Applications in Runtime Verification
- 2022
-
Ingår i: Lecture Notes in Computer Science book series (LNCS, volume 13498). - Cham : Springer, Cham. - 0302-9743 .- 1611-3349. - 9783031171956
-
Konferensbidrag (refereegranskat)abstract
- Aspect-oriented programming tools aim to provide increased code modularity by enabling programming of cross-cutting concerns separate from the main body of code. Since the inception of runtime verification, aspect-oriented programming has regularly been touted as a perfect accompanying tool, by allowing for non-invasive monitoring instrumentation techniques. In this paper we present, AspectSol, which enables aspect-oriented programming for smart contracts written in Solidity, and then discuss the design space for pointcuts and aspects in this context. We present and evaluate practical runtime verification uses and applications of the tool.
|
|
| 8. |
- Azzopardi, Shaun, 1992, et al.
(författare)
-
Tainting in Smart Contracts: Combining Static and Runtime Verification
- 2022
-
Ingår i: Lecture Notes in Computer Science book series (LNCS,volume 13498). - Cham : Springer, Cham. - 0302-9743 .- 1611-3349. - 9783031171956
-
Konferensbidrag (refereegranskat)abstract
- Smart contracts exist immutably on blockchains, making their pre-deployment correctness essential. Moreover, they exist openly on blockchains—open for interaction with any other smart contract and offchain entity. Interaction, for instance with off-chain oracles, can affect the state of the smart contract, and correctness of these smart contracts may depend on the trustworthiness of the data they manipulate or events they generate which, in turn, would depend on which parties or what information contributed to them. In this paper, we develop and present dynamic taint analysis techniques to enable data tainting in smart contracts. We propose an extension of Solidity that enables labelling inputs of interaction endpoints with dynamic data-carrying labels that capture actionable information about the sender. These labels can then be propagated dynamically across transactions to transitively dependent data. Specifications can then refer to such taints, for instance for ensuring that certain data could not have been influenced through interaction by a certain party. We further allow the use of taints as part of the language, affecting the control flow of the smart contract. To manage the overheads of such runtime tainting we develop sound static analysis-based techniques to prune away unnecessary instrumentation. We give a case study as a proof-of-concept, and measure the overheads associated with our additions before and after optimisation.
|
|
| 9. |
- Chircop, Stefan, et al.
(författare)
-
An Automata-Based Formalism for Normative Documents with Real-Time
- 2022
-
Ingår i: Frontiers in Artificial Intelligence and Applications. - : IOS Press. - 0922-6389.
-
Konferensbidrag (refereegranskat)abstract
- Deontic logics have long been the tool of choice for the formal analysis of normative texts. While various such logics have been proposed many deal with time in a qualitative sense, i.e., reason about the ordering but not timing of events, it was only in the past few years that real-time deontic logics have been developed to reason about time quantitatively. In this paper we present timed contract automata, an automata-based deontic modelling approach complementing these logics with a more operational view of such normative clauses and providing a computational model more amenable to automated analysis and monitoring.
|
|
| 10. |
- Colombo, Christian, et al.
(författare)
-
LARVA -A Tool for Runtime Monitoring of Java Programs
- 2009
-
Ingår i: IEEE Computer Society. - 9780769538709 ; , s. 33-37
-
Konferensbidrag (refereegranskat)abstract
- The use of runtime verification, as a lightweight approach to guarantee properties of systems, has been increasingly employed on real-life software. In this paper, we present a tool LARVA, for the runtime verification of real-time properties of Java programs. Properties can be expressed in a number of notations, including timed-automata enriched with stopwatches, Lustre, and a subset of duration calculus. The tool has been successfully used on a number of case-studies, including an industrial system handling financial transactions. LARVA also performs analysis of real-time properties, to calculate, if possible, an upper-bound on the memory and temporal overheads induced by monitoring. Moreover, it gives other useful information, as for instance what is the impact of monitoring the system with respect to the monitored properties.
|
|
