| 1. |
|
|
| 2. |
- Abdulla, Parosh, Professor, 1961-, et al.
(författare)
-
Consistency and Persistency in Program Verification : Challenges and Opportunities
- 2022
-
Ingår i: Principles of Systems Design. - Cham : Springer. - 9783031223365 - 9783031223372 ; , s. 494-510
-
Bokkapitel (övrigt vetenskapligt/konstnärligt)abstract
- We consider the verification of concurrent programs and, in particular, the challenges that arise because modern platforms only guarantee weak semantics, i.e., semantics that are weaker than the classical Sequential Consistency (SC). We describe two architectural concepts that give rise to weak semantics, namely weak consistency and weak persistency. The former defines the order in which operations issued by a given process become visible to the rest of the processes. The latter prescribes the order in which data becomes persistent. To deal with the extra complexity in program behaviors that arises due to weak semantics, we propose translating the program verification problem under weak semantics to SC. The main principle is to augment the program with a set of (unbounded) data structures that guarantee the equivalence of the source program’s behavior under the weak semantics with the augmented program’s behavior under the SC semantics. Such an equivalence opens the door to leverage, albeit in a non-trivial manner, the rich set of techniques that we have developed over the years for program verification under the SC semantics. We illustrate the framework’s potential by considering the persistent version of the well-known Total Store Order semantics. We show that we can capture the program behaviors on such a platform using a finite set of unbounded monotone FIFO buffers. The use of monotone FIFO buffers allows the use of the well-structured-systems framework to prove the decidability of the reachability problem.
|
|
| 3. |
|
|
| 4. |
- Andersson, Erik, et al.
(författare)
-
Ambio fit for the 2020s
- 2022
-
Ingår i: Ambio. - : Springer Nature. - 0044-7447 .- 1654-7209. ; 51:5, s. 1091-1093
-
Tidskriftsartikel (refereegranskat)
|
|
| 5. |
- Angelstam, Per, et al.
(författare)
-
Sweden does not meet agreed national and international forest biodiversity targets : A call for adaptive landscape planning
- 2020
-
Ingår i: Landscape and Urban Planning. - : Elsevier BV. - 0169-2046 .- 1872-6062. ; 202
-
Tidskriftsartikel (refereegranskat)abstract
- Loss of forest naturalness challenges the maintenance of green infrastructure (GI) for biodiversity conservation and delivery of diverse ecosystem services. Using the Convention on Biological Diversity's Aichi target #11 with its quantitative and qualitative criteria as a normative model, we aim at supporting landscape planning through a pioneering assessment of the extent to which existing amounts and spatial distributions of High Conservation Value Forests (HCVFs) meet these criteria. Highly forested and committed to both intensive wood production and evidence-based conservation targets of 17–20% protected areas, Sweden was chosen as a case study. Specifically, we estimated the amount, regional representation, and functional connectivity of HCVF patches using virtual bird species, validated the results using field surveys of focal bird species, and assessed conservation target fulfilment. Finally, we linked these results to the regional distribution of forest land ownership categories, and stress that these provide different opportunities for landscape planning. Even if 31% of forest land in Sweden is officially protected, voluntarily set-aside, or not used for wood production now and in the future, we show that applying the representation and connectivity criteria of Aichi target #11 reduces this figure to an effective GI of 12%. When disaggregating the five ecoregions the effective GI was 54% for the sub-alpine forest ecoregion, which hosts EU's last intact forest landscapes, but only 3–8% in the other four ecoregions where wood production is predominant. This results in an increasing need for forest habitat and landscape restoration from north to south. The large regional variation in the opportunity for landscape planning stresses the need for a portfolio of different approaches. We stress the need to secure funding mechanisms for compensating land owners’ investments in GI, and to adapt both the approaches and spatial extents of landscape planning units to land ownership structure.
|
|
| 6. |
- Arnqvist, Goran, et al.
(författare)
-
Falsk marknadsföring om hållbart skogsbruk
- 2022
-
Ingår i: Svenska Dagbladet Debatt. - 1101-2412.
-
Tidskriftsartikel (populärvet., debatt m.m.)abstract
- Dagens svenska skogsbruk är inte ekologiskt hållbart. Att saluföra det som hållbart är därför – för att tala klarspråk – falsk marknadsföring, skriver forskare.
|
|
| 7. |
- Asadian, Hooman, et al.
(författare)
-
Applying Symbolic Execution to Test Implementations of a Network Protocol Against its Specification
- 2022
-
Ingår i: 2022 IEEE 15TH INTERNATIONAL CONFERENCE ON SOFTWARE TESTING, VERIFICATION AND VALIDATION (ICST 2022). - : Institute of Electrical and Electronics Engineers (IEEE). - 9781665466790 - 9781665466806 ; , s. 70-81
-
Konferensbidrag (refereegranskat)abstract
- Implementations of network protocols must conform to their specifications in order to avoid security vulnerabilities and interoperability issues. We describe our experiences using symbolic execution to thoroughly test several implementations of a network security protocol against its specification. We employ a methodology in which we first extract requirements from the protocol's RFC and turn them into formulas. These formulas are then utilized by symbolically executing the protocol implementation to explore code paths that can be traversed on packet sequences that violate a requirement. When this exploration exposes a bug, corresponding input values are produced and turned into test cases that can validate the bug in the original implementation. Since we let symbolic execution be guided by requirements, it can naturally produce a wide variety of requirement-violating input sequences, which is difficult to achieve with existing techniques for protocol testing. We applied this methodology to test four different implementations of MILS against the protocol's RFC. We were able to quickly expose a known CVE in an older version of OpenSSL, and to discover numerous previously unknown vulnerabilities and nonconformance issues in DTI.S implementations, which have by now been confirmed and fixed by their implementors.
|
|
| 8. |
- Bakidou, Anna, 1996, et al.
(författare)
-
On Scene Injury Severity Prediction (OSISP) model for trauma developed using the Swedish Trauma Registry
- 2023
-
Ingår i: BMC Medical Informatics and Decision Making. - 1472-6947. ; 23:1
-
Tidskriftsartikel (refereegranskat)abstract
- Background: Providing optimal care for trauma, the leading cause of death for young adults, remains a challenge e.g., due to field triage limitations in assessing a patient’s condition and deciding on transport destination. Data-driven On Scene Injury Severity Prediction (OSISP) models for motor vehicle crashes have shown potential for providing real-time decision support. The objective of this study is therefore to evaluate if an Artificial Intelligence (AI) based clinical decision support system can identify severely injured trauma patients in the prehospital setting. Methods: The Swedish Trauma Registry was used to train and validate five models – Logistic Regression, Random Forest, XGBoost, Support Vector Machine and Artificial Neural Network – in a stratified 10-fold cross validation setting and hold-out analysis. The models performed binary classification of the New Injury Severity Score and were evaluated using accuracy metrics, area under the receiver operating characteristic curve (AUC) and Precision-Recall curve (AUCPR), and under- and overtriage rates. Results: There were 75,602 registrations between 2013–2020 and 47,357 (62.6%) remained after eligibility criteria were applied. Models were based on 21 predictors, including injury location. From the clinical outcome, about 40% of patientswere undertriaged and 46% were overtriaged. Models demonstrated potential for improved triaging and yielded AUC between 0.80–0.89 and AUCPR between 0.43–0.62. Conclusions: AI based OSISP models have potential to provide support during assessment of injury severity. The findings may be used for developing tools to complement field triage protocols, with potential to improve prehospital trauma care and thereby reduce morbidity and mortality for a large patient population.
|
|
| 9. |
- Borg, Tor, et al.
(författare)
-
Mått på bostadsbristen : Förslag på hur återkommande bedömningar ska utföras
- 2020
-
Rapport (övrigt vetenskapligt/konstnärligt)abstract
- Boverket fick i juni 2019 i uppdrag av regeringen att lämna förslag på hur återkommande bedömningar av bostadsbristen ska utföras samt att lämna förslag på enhetliga begrepp som ska användas vid kommunikation kring bostadsbristen. Avsikten är att de presenterade beräkningarna ska kunna användas i arbetet med bostadsförsörjningsfrågor och underlätta arbetet med att planera, utföra och följa upp insatser för att åtgärda bostadsbristen. Boverket har tagit fram en årlig beräkningsmodell där antalet hushåll som saknar en rimlig bostad beräknas på både nationell, regional och lokal nivå. Vad som är en rimlig bostad definieras enligt en uppsättning kriterier och normer. Kvantitativa mått visar hur många hushåll som har en boendesituation som inte uppfyller de olika kriterierna. Samråd har skett med Sveriges Kommuner och Regioner (SKR) samt med Socialstyrelsen under uppdragets gång. Båda anser att de givits utrymme att framföra sin mening och har förklarat sig nöjda med samrådet. Avstämningar har också gjorts med en rad andra aktörer. Denna rapport utgör Boverkets slutredovisning av uppdraget. Rapporten har tagits fram av en projektgrupp bestående av Tor Borg, Bengt J Eriksson, Oskar Gramstad, Ulla-Christel Götherström, Hans Jonsson, Bo Söderberg och Hang Zettervall, med den förstnämnda som projektledare.
|
|
| 10. |
- Bubnicki, Jakub W., et al.
(författare)
-
The conservation value of forests can be predicted at the scale of 1 hectare
- 2024
-
Ingår i: Communications Earth & Environment. - : Springer Nature. - 2662-4435. ; 5:1
-
Tidskriftsartikel (refereegranskat)abstract
- To conserve biodiversity, it is imperative to maintain and restore sufficient amounts of functional habitat networks. Therefore, the location of the remaining forests with natural structures and processes over landscapes and large regions is a key objective. Here we integrated machine learning (Random Forest) and open landscape data to scan all forest landscapes in Sweden with a 1 ha spatial resolution with respect to the relative likelihood of hosting High Conservation Value Forests. Using independent spatial stand- and plot-level validation data, we confirmed that our predictions correctly represent different levels of forest naturalness, from degraded to those with high and associated biodiversity conservation values. Given ambitious national and international conservation objectives and increasingly intensive forestry, our model and the resulting wall-to-wall mapping fill an urgent gap for assessing the achievement of evidence-based conservation targets, spatial planning, and designing forest landscape restoration.
|
|
